aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-13 23:40:33 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-13 23:40:33 +0200
commitf824657b2b0b42ff02d0c07337db1607e13f359f (patch)
tree22f06b457451e88dcea25d190ec954021c800d77 /configure.ml
parentef62eddc084784fdc001e3e304a73a73568e7b8a (diff)
parent6cdc4c69ea57f0498cc36f5213268920ca7f7d63 (diff)
Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of the Reference Manual (Introduction, Credits).
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions