Don't recreate old docs (#5243)

2020-06-24 09:59:07 -04:00
parent b29683736a
commit 64c393ee74
1 changed files with 1 additions and 1 deletions
--- a/.circleci/deploy.sh
+++ b/.circleci/deploy.sh
@@ -5,7 +5,7 @@ function deploy_doc(){
 	git checkout $1
 	if [ ! -z "$2" ]
 	then
-		if [ -d "$dir/$2" ]; then
+		if [ "$2" != "master" ] && ssh -oStrictHostKeyChecking=no $doc "[ -d $dir/$2 ]"; then
 			echo "Directory" $2 "already exists"
 		else
 			echo "Pushing version" $2