diff options
| author | Maxime Dénès | 2017-07-17 07:32:44 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-17 07:32:44 +0200 |
| commit | e3c4da34f14b00d2b3feb087fcce1cebd8064064 (patch) | |
| tree | d9f066b10b1b3b1129bf8bb53ffd5ed2f262e82f /plugins/syntax/string_syntax.ml | |
| parent | 7359b3e756e4472282c212b99fd7a1926a2fea47 (diff) | |
| parent | 8f2c2a758f3d5e01238760be12c83d4ff08d5276 (diff) | |
Merge PR #865: RefMan-ext: fix some typos
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions