Remove unused file (#6023)

This commit is contained in:
Sylvain Gugger 2020-07-27 08:31:24 -04:00 committed by GitHub
parent b9b11795cf
commit 3b64ad5d5c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -1,23 +0,0 @@
cd docs
function deploy_doc(){
echo "Creating doc at commit $1 and pushing to folder $2"
git checkout $1
if [ ! -z "$2" ]
then
echo "Pushing version" $2
make clean && make html && scp -r -oStrictHostKeyChecking=no _build/html $doc:$dir/$2
else
echo "Pushing master"
make clean && make html && scp -r -oStrictHostKeyChecking=no _build/html/* $doc:$dir
fi
}
deploy_doc "master"
deploy_doc "b33a385" v1.0.0
deploy_doc "fe02e45" v1.1.0
deploy_doc "89fd345" v1.2.0
deploy_doc "fc9faa8" v2.0.0
deploy_doc "3ddce1d" v2.1.1
deploy_doc "f2f3294" v2.2.0
deploy_doc "d0f8b9a" v2.3.0