diff options
| author | Maxime Dénès | 2018-11-23 13:12:02 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-27 15:09:19 +0100 |
| commit | 3bffd4f4f4a9ef400781aa7a4f90a986891bb0c1 (patch) | |
| tree | d54a59e4451ede662f70d1efb5ca2bf987d41f31 /dev/ci/gitlab.bat | |
| parent | 0a699c7c932352f38c14f1bdf33ee7955241c1d8 (diff) | |
Remove -async-proofs-full flag
The semantics of this flag was not clear, it had several rather
orthogonal effects. Also, it should probably have been another value of
`-async-proofs-mode`, rather than a separate flag, as its combination
with e.g. `-async-proofs-mode off` is unclear.
Diffstat (limited to 'dev/ci/gitlab.bat')
0 files changed, 0 insertions, 0 deletions