aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-05-20 10:28:17 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-05-20 10:28:17 +0200
commitaae960fc0ed0a3a8d244c1c3d7c5363c17044cbc (patch)
tree0687c0311c15bd7be199ea674945883d4c6f25bd /configure.ml
parent9f11adda4bff194a3c6a66d573ce7001d4399886 (diff)
Mention ./configure in INSTALL.doc
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions