From 7bbaefad7ae6c66a74a648b118d4b4c40ee95800 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Fri, 5 Oct 2018 11:40:45 +0200
Subject: Remove old folder delete (can interfere with unique folder creation)

---
 dev/ci/gitlab.bat | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'dev/ci/gitlab.bat')

diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index c7a32fd4d2..f6fe0dbb2b 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -37,9 +37,6 @@ SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/%
 SET COQREGTESTING=Y
 SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin
 
-if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build
-if exist %DESTCOQ%\ rd /s /q %DESTCOQ%
-
 IF "%WINDOWS_ALL_ADDONS%" == "enabled" (
   SET EXTRA_ADDONS=^
     -addon=mathcomp ^
-- 
cgit v1.2.3