diff options
| author | Maxime Dénès | 2016-11-02 16:46:34 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-02 16:46:34 +0100 |
| commit | 5358515f23d1cd47d4914c55dcf049df858b9dc7 (patch) | |
| tree | c9f32913dfd2bf5be65fad7c62d6e55b7a5ebd1c /kernel/nativecode.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 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions