diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-08-30 09:34:10 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-08-30 09:37:08 +0200 |
| commit | 64e801cce80ac0d3bffcebf414d57785a2c6826f (patch) | |
| tree | 645e329d85de7b34dbf3080b0048408a1719e116 /plugins/micromega | |
| 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 'plugins/micromega')
0 files changed, 0 insertions, 0 deletions