[Doc] Bugfix for gh_deploy_doc.sh (#78)

flashinfer-ai · Jan 20, 2024 · 807d197 · 807d197
1 parent 166f57b
commit 807d197
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/scripts/gh_deploy_doc.sh b/scripts/gh_deploy_doc.sh
@@ -4,16 +4,18 @@
 
 set -euxo pipefail
 
+mkdir -p tmp
 cd docs
 make html
-mv _build/html/* .
+mv _build/html/* ../tmp/
 rm -rf _build/
 cd ..
 
 git grep --cached -l '' | xargs rm
 git fetch
 git checkout -B gh-pages origin/gh-pages
 echo "3rdparty/" >> .gitignore
+mv tmp/* docs/
 
 DATE=`date`
 git add . && git commit -am "Build at ${DATE}"