diff options
| author | Hugo Herbelin | 2015-07-30 18:05:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 15:06:53 +0200 |
| commit | 1eb48ca8695a26fa5ca248a2201a164f90885360 (patch) | |
| tree | 10e488654dff10055efeb63cbd941b35b7fa7646 /kernel/type_errors.mli | |
| parent | 71e0a34f89d03787003df1a30bb793bd71ebb775 (diff) | |
For convenience, making yes and on, and no and off synonymous in
command line. Documenting only the former for simplicity and
uniformity with predating option -with-geoproof.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions