aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorVincent Laporte2019-04-01 09:23:19 +0000
committerVincent Laporte2019-04-01 12:07:05 +0000
commit4d50b90cb4e78c9e5e0bb5395ffb6c13ae72c1b1 (patch)
treef8598bd4fd916085514b5745e9b0d56b73b829d2 /dev/ci
parentf1930877e20379e11c4d6b79283980a4253c178d (diff)
[CI] Disable Coquelicot on Windows
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/gitlab.bat2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 5f819f31f9..cc1931d13d 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -49,9 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
-addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
- -addon=coquelicot ^
-addon=vst ^
-addon=aactactics
+REM -addon=coquelicot ^
) ELSE (
SET "EXTRA_ADDONS= "
)