diff options
| author | Pierre-Marie Pédrot | 2015-12-18 17:30:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-21 19:36:38 +0100 |
| commit | 589130e87d68227d25800e7506666eaf1d47a25a (patch) | |
| tree | ff7ae021ca3c3306bbcbc8b9575b3b23b78320ce /plugins/syntax/string_syntax.ml | |
| parent | 329b5b9ed526d572d7df066dc99486e1dcb9e4cc (diff) | |
Changing the toplevel type of the int_or_var generic type to int.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions