diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-04-26 11:33:14 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-26 11:33:14 +0200 |
commit | 5aa07e9eb97f6233f47aa8a79fb0890fca14f427 (patch) | |
tree | 7598436abc10861b33b7ea97a8458d6a78a3e204 /configure.ml | |
parent | 68b576a178c057a016c7d4be1b319cc8fcbfac25 (diff) | |
parent | 0900b007973759a0fea20c0395e40c6f34bed8dc (diff) |
Merge PR #7331: Fix a typo in the reference manual: <; -> <:
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions