diff options
Diffstat (limited to '.gitlab/gen_ci.hs')
| -rwxr-xr-x | .gitlab/gen_ci.hs | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/.gitlab/gen_ci.hs b/.gitlab/gen_ci.hs index 456d7f2257..5badde02d5 100755 --- a/.gitlab/gen_ci.hs +++ b/.gitlab/gen_ci.hs @@ -908,8 +908,10 @@ job_groups = { bignumBackend = Native } , make_wasm_jobs wasm_build_config - , disableValidate $ make_wasm_jobs wasm_build_config { bignumBackend = Native } - , disableValidate $ make_wasm_jobs wasm_build_config { unregisterised = True } + , modifyValidateJobs manual $ + make_wasm_jobs wasm_build_config {bignumBackend = Native} + , modifyValidateJobs manual $ + make_wasm_jobs wasm_build_config {unregisterised = True} , addValidateRule NonmovingGc (standardBuildsWithConfig Amd64 (Linux Debian11) vanilla {validateNonmovingGc = True}) ] |