diff --git a/deploy_docs.sh b/deploy_docs.sh index 2f77858..d9d89bc 100755 --- a/deploy_docs.sh +++ b/deploy_docs.sh @@ -23,7 +23,7 @@ fi # generate the docs cd $1 -../$2/build/bin/doc-gen4 /mathlib4_docs/ Mathlib +../$2/build/bin/doc-gen4 Mathlib if [ "$3" = "true" ]; then cd ..