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.ml | |
| 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.ml')
0 files changed, 0 insertions, 0 deletions