diff options
| author | Hugo Herbelin | 2014-12-16 16:28:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-16 16:28:34 +0100 |
| commit | 22aa11b21202a44c35da70970da6b34479c4a815 (patch) | |
| tree | aa4dcbecaac9da0e0e637b6e04413359b7a7f171 /plugins/syntax/string_syntax.ml | |
| parent | eed9b6ba37f6eeb1c9e8858a82c257cd69837e55 (diff) | |
In CHANGES, alerting about stronger check on notation level modifiers.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions