diff options
author | 2016-08-30 09:34:10 +0200 | |
---|---|---|
committer | 2016-08-30 09:37:08 +0200 | |
commit | 64e801cce80ac0d3bffcebf414d57785a2c6826f (patch) | |
tree | 645e329d85de7b34dbf3080b0048408a1719e116 /printing/miscprint.ml | |
parent | 513e194656429b6a9142a3a34095cee2c6f8ee96 (diff) |
Setting an unknown option now always a warning. Fixes #4947.
Previously, setting an unknown option was an error or a warning,
depending on the type of the option. We make it always a warning, for
forward compatibility.
This was already fixed in 8.6.
Diffstat (limited to 'printing/miscprint.ml')
0 files changed, 0 insertions, 0 deletions