From e8b7c1bd1e4e6a1ac005b5eb299d0ef946b83c96 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Sun, 30 Sep 2018 19:59:41 +0200
Subject: Fix issue 8603 Move Windows CI runs to folder C:/ci

---
 dev/ci/gitlab.bat | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 31bd65af08..a848c49d75 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -8,23 +8,24 @@ TIME /T
 REM List currently used cygwin and target folders for debugging / maintenance purposes
 
 ECHO "Currently used cygwin folders"
-DIR C:\cygwin*
+DIR C:\ci\cygwin*
 ECHO "Currently used target folders"
-DIR C:\coq*
+DIR C:\ci\coq*
+ECHO "Root folders"
+DIR C:\
 
 if %ARCH% == 32 (
   SET ARCHLONG=i686
-  SET CYGROOT=C:\cygwin
   SET SETUP=setup-x86.exe
 )
 
 if %ARCH% == 64 (
   SET ARCHLONG=x86_64
-  SET CYGROOT=C:\cygwin64
   SET SETUP=setup-x86_64.exe
 )
 
-SET DESTCOQ=C:\coq%ARCH%_inst
+SET CYGROOT=C:\ci\cygwin%ARCH%
+SET DESTCOQ=C:\ci\coq%ARCH%
 
 CALL :MakeUniqueFolder %CYGROOT% CYGROOT
 CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ
@@ -93,9 +94,9 @@ GOTO :EOF
 
 :CleanupFolders
   ECHO "Cleaning %CYGROOT%"
-  DEL /S /F /Q "%CYGROOT%" > NUL
+  RMDIR /S /Q "%CYGROOT%"
   ECHO "Cleaning %DESTCOQ%"
-  DEL /S /F /Q "%DESTCOQ%" > NUL
+  RMDIR /S /Q "%DESTCOQ%"
   GOTO :EOF
 
 :MakeUniqueFolder
-- 
cgit v1.2.3