diff options
| author | Gaëtan Gilbert | 2019-09-24 14:53:04 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-09-24 14:53:04 +0200 |
| commit | 90553b5ca20f2acc9803baf0cf487eb34b6c8f12 (patch) | |
| tree | a6e06854ad02f9106ca88b00c37588535e12b563 /plugins/syntax/string_notation.mli | |
| parent | 35c997c5c2ab6ee2f29fbeb548359e63c23a1394 (diff) | |
| parent | 7b59d8c9d9b2104de7162ec0e40f6182a6830046 (diff) | |
Merge PR #10699: [gitlab/ci] Prevent Corn from running if Bignums has failed.
Reviewed-by: SkySkimmer
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions