Fix deploy doc (#5246)

* Try with the same command

* Try like this
This commit is contained in:
Sylvain Gugger
2020-06-24 10:59:06 -04:00
committed by GitHub
parent 49f6e7a3c6
commit f216b60671

View File

@@ -9,10 +9,15 @@ function deploy_doc(){
echo "Directory" $2 "already exists" echo "Directory" $2 "already exists"
else else
echo "Pushing version" $2 echo "Pushing version" $2
make clean && make html && scp -r -oStrictHostKeyChecking=no _build/html $doc:$dir/$2 make clean && make html
if [ "$2" == "master" ]; then
scp -r -oStrictHostKeyChecking=no _build/html/* $doc:$dir/$2/
else
scp -r -oStrictHostKeyChecking=no _build/html $doc:$dir/$2
fi
fi fi
else else
echo "Pushing master" echo "Pushing stable"
make clean && make html && scp -r -oStrictHostKeyChecking=no _build/html/* $doc:$dir make clean && make html && scp -r -oStrictHostKeyChecking=no _build/html/* $doc:$dir
fi fi
} }