diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-10 13:24:54 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-14 14:17:11 +0100 |
| commit | 8fe6da32544ee73201f7c64b3dd45afb56c75b71 (patch) | |
| tree | 52c1c123d184fd4d32cc48243245c1012ee5afd5 /configure.ml | |
| parent | 30f222b1aad7ec483902b74dfa7dad7aefd5fca3 (diff) | |
Fix bug in warnings: -w foo was silent when foo did not exist.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions