diff options
| author | Enrico Tassi | 2020-01-03 19:09:15 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-01-03 19:09:15 +0100 |
| commit | 793bddef6b4f615297e9f9088cd0b603c56b2014 (patch) | |
| tree | bff9cb13225836a72ebed11044636204b7537eb3 /plugins/syntax/string_notation.ml | |
| parent | fbd911ee701a63a05c213cfe6e98271fa54c874a (diff) | |
| parent | c380202139b158647089c1352bcacf82c99012ea (diff) | |
Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issue
Reviewed-by: gares
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions