diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-26 14:33:07 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-26 14:34:46 +0100 |
| commit | f712a0523359d5b54b4d4160bc77271fdde094a3 (patch) | |
| tree | 1408eabb7d2cb58117a3a82fe2ce2161470c9f05 /lib/pp.ml | |
| parent | c8944dccb081c79eb47ca91c7e2cb5c50558aeaa (diff) | |
Mention -R option in warnings, fixing #4067 and #4068.
Diffstat (limited to 'lib/pp.ml')
0 files changed, 0 insertions, 0 deletions