diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-01 18:24:16 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-01 19:50:14 +0100 |
commit | bca756eaebf16b6145c65b53629219d2a0a8b1ba (patch) | |
tree | ef95ccc25c75c7d173af5bf10c2de2d397f875c7 /plugins/xml/xml_plugin.mllib | |
parent | 4cddb7d0765a091c6514a85475dcdd7af34aaf29 (diff) |
Better behaviour for sets of reserved names.
Diffstat (limited to 'plugins/xml/xml_plugin.mllib')
0 files changed, 0 insertions, 0 deletions