diff options
| author | Maxime Dénès | 2019-07-22 09:34:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-07-22 09:34:15 +0200 |
| commit | 8ccafba4844c16ac4668bcb8475f3fb1d69c28ca (patch) | |
| tree | 959f41196339a8516ca6b0dec693d66d8016e991 /dev/ci/gitlab.bat | |
| parent | cd6fc50854285f02bf151e94bdfb819988531fd2 (diff) | |
| parent | 7341d286d4a9b440810097352fe257e476a8903c (diff) | |
Merge PR #10522: Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)
Reviewed-by: vbgl
Diffstat (limited to 'dev/ci/gitlab.bat')
| -rwxr-xr-x | dev/ci/gitlab.bat | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 6c4ccfc14d..3998fc6514 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -48,9 +48,13 @@ IF "%WINDOWS%" == "enabled_all_addons" ( -addon=compcert ^
-addon=extlib ^
-addon=quickchick ^
+ -addon=coquelicot ^
-addon=vst ^
- -addon=aactactics
-REM -addon=coquelicot ^
+ -addon=aactactics ^
+ -addon=flocq ^
+ -addon=interval ^
+ -addon=gappa_tool ^
+ -addon=gappa
) ELSE (
SET "EXTRA_ADDONS= "
)
|