aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.mli
diff options
context:
space:
mode:
authorHugo Herbelin2020-03-04 21:09:22 +0100
committerHugo Herbelin2020-03-22 15:02:43 +0100
commitf7687371270e0b3fd3b61db3f25128c567aa7033 (patch)
treef0a87ead339228ccc401b15ba12824aaf538ac6b /plugins/syntax/string_notation.mli
parent8b8a612940127084d0162408eda5a1fe77365e79 (diff)
Adding support for parsing "+" sig in NumTok.
Support in the parser needs yet to be added though.
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions