From 903a5a0d837c75cbf1c23fead4672e5d21354869 Mon Sep 17 00:00:00 2001
From: Chengnian Sun <chengniansun@gmail.com>
Date: Tue, 7 Nov 2023 09:27:29 -0500
Subject: [PATCH] prepare for the next release

---
 scripts/copy_to_public_repo.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/scripts/copy_to_public_repo.sh b/scripts/copy_to_public_repo.sh
index f2562234d..7a6d684d3 100755
--- a/scripts/copy_to_public_repo.sh
+++ b/scripts/copy_to_public_repo.sh
@@ -50,5 +50,8 @@ for entry in $(git -C "$PUBLIC_REPO_DIR" ls-tree --name-only HEAD); do
   cp -rf "$(basename "${entry}")" "${PUBLIC_REPO_DIR}/"
 done
 
+for entry in $(find . -maxdepth 1 -type f); do
+  cp "${entry}" "${PUBLIC_REPO_DIR}/"
+done
 echo
 echo "Done."