diff options
Diffstat (limited to 'dev/ci/gitlab.bat')
| -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 ^
|