aboutsummaryrefslogtreecommitdiffstats
path: root/configure
diff options
context:
space:
mode:
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure2
1 files changed, 1 insertions, 1 deletions
diff --git a/configure b/configure
index 53346109..3d0196fb 100755
--- a/configure
+++ b/configure
@@ -70,7 +70,7 @@ Options:
-no-runtime-lib Do not compile nor install the runtime support library
-no-standard-headers Do not install nor use the standard .h headers
-clightgen Also compile the clightgen tool
- -ignore-coq-version Accept touse experimental or unsupported versions of Coq
+ -ignore-coq-version Accept to use experimental or unsupported versions of Coq
'