From 64c393ee74a2294d1608dc327a997683b4ea689e Mon Sep 17 00:00:00 2001
From: Sylvain Gugger <35901082+sgugger@users.noreply.github.com>
Date: Wed, 24 Jun 2020 09:59:07 -0400
Subject: [PATCH] Don't recreate old docs (#5243)

---
 .circleci/deploy.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.circleci/deploy.sh b/.circleci/deploy.sh
index 0008b23494..b95113c679 100755
--- 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