aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-06 17:37:05 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-06 17:37:05 +0200
commit870d1e06bc27ae7b108570eeaf9707041e9ff191 (patch)
tree94fc0b3ab553e5a8bda3a36cc469e51f6ef3e312 /configure.ml
parent0387d0c1cca76dbcc6a55aadb3198e4868a83112 (diff)
Fix typo in configure (noticed by Jason).
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index aee386b49..6748da1d8 100644
--- a/configure.ml
+++ b/configure.ml
@@ -13,7 +13,7 @@ open Printf
let coq_version = "8.5pl2"
let coq_macos_version = "8.5.2" (** "[...] should be a string comprised of
-three non-negative, period-separed integers [...]" *)
+three non-negative, period-separated integers [...]" *)
let vo_magic = 8500
let state_magic = 58500
let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";