diff options
| author | larsr | 2020-03-12 17:20:18 +0100 |
|---|---|---|
| committer | GitHub | 2020-03-12 17:20:18 +0100 |
| commit | 3f2bfa50b1063bc981e3edfb8f5c6eaf53253643 (patch) | |
| tree | ae574fd4a357653a04130fb2d6703637f6a16dc1 /plugins/syntax/string_notation.mli | |
| parent | 1a7cdc1da9bff2e46acdd5c07a7eee5dcd27d731 (diff) | |
Fixed link to "match" syntax.
and removed the now incorrect "section 8.2.3" reference, as it is the same as the "refine" link.
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions