diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-13 18:11:45 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 15:05:04 +0100 |
| commit | cee56f902fdae8a3de13ea93f0209f08ac256b08 (patch) | |
| tree | 77a77167d51dc5212d823996e7ee2a030c869894 /library/global.ml | |
| parent | 9a1bbeee7712f21d55cc352020ff51203cac7c51 (diff) | |
Arguments: warn only if no option is given (Close 3860)
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions