diff options
| author | Gaëtan Gilbert | 2018-05-14 13:43:55 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-14 13:45:27 +0200 |
| commit | eed834b337354251dfd0ae60c8358f4d126420b2 (patch) | |
| tree | a68b66e9a5f795d971070afdc6948d8709f6ffde /kernel/cbytecodes.mli | |
| parent | 4094a8c2cac668db112fc84f5d1b287eacbf6700 (diff) | |
gitlab CI: fix [warnings] template
We never actually used the -warn-error flag...
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions