diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-11-13 15:56:47 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-01-15 17:26:48 +0100 |
commit | d6d81d63591e37fd74c841165afd9e3baf6e0d8d (patch) | |
tree | 647a48294185eb53345884989dbfca1bf82f56e0 /library/lib.mli | |
parent | 65b45fe6e86cc8b642069e33c3b7073f48b592a9 (diff) |
Fix #4408.
Removed documentation for broken -D -w (but the option are still there).
Fixed documentation of others.
Diffstat (limited to 'library/lib.mli')
0 files changed, 0 insertions, 0 deletions