diff options
| author | Hugo Herbelin | 2018-09-24 12:05:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-24 12:05:53 +0200 |
| commit | a3f598cdfe681c7b0e77cbd8d9778f1920683c77 (patch) | |
| tree | efa06408e6c13c0a98b5783d2e548404474c8f98 /plugins/syntax/string_syntax.ml | |
| parent | 5764e978a30c21f017741b984bc60a4f7b94faf8 (diff) | |
| parent | e186109404b665d79bf441f8d1ccee39cc76b165 (diff) | |
Merge PR #8530: Fix typo in comment.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions