diff options
Diffstat (limited to 'dev/ci/gitlab.bat')
| -rwxr-xr-x | dev/ci/gitlab.bat | 2 |
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= "
)
|