diff options
| author | Pierre-Marie Pédrot | 2016-09-02 14:04:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-02 14:04:18 +0200 |
| commit | f60d849a9601febc35a35204d2442e72673e3fb4 (patch) | |
| tree | 1069fe749f3c0c3474dce8d82f5d1272d54a9bd2 /engine | |
| parent | 675d7c4310e10d68e876331a95c46b726494ed91 (diff) | |
Silence the CAMLP5 warnings on command line.
They were mostly useless, and people complained about it. Not that because
there is no API to make CAMLP4 silent, a CAMLP4-based Coq will still spit
out its share of noisy warnings.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions