diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-12 23:41:19 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-12 23:41:19 +0200 |
commit | 8a388cd914f8c8359f7637ade728f3a9ac5a291b (patch) | |
tree | a98fdf1c98164e93c2b71a7a6dff5647cd0079e1 /tools/ocamllibdep.mll | |
parent | cbc85b215c398d0475d8347ce4d37bfb4d37d883 (diff) | |
parent | a069562bc0d4e82f6b1587864a8297b21a3250cc (diff) |
Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes`
Diffstat (limited to 'tools/ocamllibdep.mll')
0 files changed, 0 insertions, 0 deletions