diff options
| author | Enrico Tassi | 2016-09-30 11:08:47 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-30 11:08:47 +0200 |
| commit | 69d43e7615f080c2e4e57a87e84b51be857ab678 (patch) | |
| tree | 6ec8c9e43a3e035cab88018c113e7b840965d882 /kernel/type_errors.ml | |
| parent | 775b8f28562d1d5063da2b28a06e59610b76f06f (diff) | |
Restore code ignoring <W> lines in output (camlp5 warnings)
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions