diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-10 13:24:28 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-14 14:17:11 +0100 |
| commit | 30f222b1aad7ec483902b74dfa7dad7aefd5fca3 (patch) | |
| tree | 9a4106bf39d7ec15b07e845324844ea25160ced8 /configure.ml | |
| parent | 7e992fa784ee6fa48af8a2e461385c094985587d (diff) | |
Do not mention "none" in warnings doc, as it is there for compatibility.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions