diff options
| author | Michael Soegtrop | 2018-10-05 11:40:45 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2018-10-05 14:07:06 +0200 |
| commit | 7bbaefad7ae6c66a74a648b118d4b4c40ee95800 (patch) | |
| tree | 84b3b0fae911c7670ba27b328cc02416bb67896f /dev/ci | |
| parent | 4bd1bb0091d2e69637444b776f6025a4b1c049b7 (diff) | |
Remove old folder delete (can interfere with unique folder creation)
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/gitlab.bat | 3 |
1 files changed, 0 insertions, 3 deletions
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 ^
|