modify deploy_docs to not need relative path

2022-04-07 00:44:49 +01:00 · 2022-04-07 00:44:49 +01:00 · f5b9e02766
parent 9eec1cf1ad
commit f5b9e02766
1 changed files with 1 additions and 1 deletions
--- 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 ..