diff options
| author | Pierre-Marie Pédrot | 2020-03-12 15:11:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:44:50 +0100 |
| commit | 96ec58df041dc0111df0e681269aed9d0e9b571a (patch) | |
| tree | 7abcbb4ec26dfd3fb2ac81934d6e8c8602cc7d80 /plugins/syntax/string_notation.ml | |
| parent | 245b94cd075b6be527590c425a98262d89577909 (diff) | |
Use a 3-valued flag for hint locality.
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions