aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMichael Soegtrop2018-12-11 14:15:38 +0100
committerMichael Soegtrop2018-12-12 09:12:26 +0100
commit393f21c30921de34d48b751f6d8d50758982be4c (patch)
tree414e8901cd01f46531ffb48a8f334c07620da347 /dev
parentccd5cf3c0fa3248bcfc6c37b5693fc0e5ea6ac61 (diff)
Fix issue #9188 : Enable VST and aactactics in master
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/gitlab.bat7
1 files changed, 3 insertions, 4 deletions
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 386a3de204..2a42a6b58e 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -49,10 +49,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
-addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
- -addon=coquelicot
- REM addons with build issues
- REM -addon=vst ^
- REM -addon=aactactics ^
+ -addon=coquelicot ^
+ -addon=vst ^
+ -addon=aactactics
) ELSE (
SET "EXTRA_ADDONS= "
)