diff options
| author | Théo Zimmermann | 2018-07-13 23:40:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-13 23:40:33 +0200 |
| commit | f824657b2b0b42ff02d0c07337db1607e13f359f (patch) | |
| tree | 22f06b457451e88dcea25d190ec954021c800d77 /plugins/syntax/string_syntax.ml | |
| parent | ef62eddc084784fdc001e3e304a73a73568e7b8a (diff) | |
| parent | 6cdc4c69ea57f0498cc36f5213268920ca7f7d63 (diff) | |
Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of the Reference Manual (Introduction, Credits).
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions