diff options
author | 2016-11-02 16:46:34 +0100 | |
---|---|---|
committer | 2016-11-02 16:46:34 +0100 | |
commit | 5358515f23d1cd47d4914c55dcf049df858b9dc7 (patch) | |
tree | c9f32913dfd2bf5be65fad7c62d6e55b7a5ebd1c /lib/util.ml | |
parent | 0d06d69ffc0436ed326bf3e4c684dc17a4d85dde (diff) |
Better Arguments compatibility.
With multiple arguments list, repeating the "/" modifier used to be
mandatory. So instead of forbidding it, we issue a deprecation warning.
Diffstat (limited to 'lib/util.ml')
0 files changed, 0 insertions, 0 deletions