diff options
| author | Pierre-Marie Pédrot | 2014-03-01 16:02:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-01 16:02:34 +0100 |
| commit | 124734fd2c523909802d095abb37350519856864 (patch) | |
| tree | 177d3fe6ed5fe665a7151601802eb4bb09b9e0eb /plugins/syntax/string_syntax.ml | |
| parent | 9e2ee5801ae37e54dfac34f27ed2f07bbb8322d3 (diff) | |
Useless check when loading notations through import.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions