diff options
| author | Maxime Dénès | 2019-01-17 16:49:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-17 16:49:13 +0100 |
| commit | 2e231b0eb3d107aedc7a26dc173d6ac00cb3473f (patch) | |
| tree | 05caa777a0e233bd47b603fd109f4318f076f637 /dev/ci/gitlab.bat | |
| parent | f50256c7b4a75a59bb25a78431f0b24ae1046bf3 (diff) | |
| parent | 393f21c30921de34d48b751f6d8d50758982be4c (diff) | |
Merge PR #9192: Issue #9175, #9190, #9191 (various minor Windows build issues)
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/ci/gitlab.bat')
| -rwxr-xr-x | dev/ci/gitlab.bat | 7 |
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= "
)
|