aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b0d90f2cb..ba20c771a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1377,7 +1377,7 @@ let check_for_geoproof_input () =
full name, with the last occurrence of "coqide" replaced by "coqtop".
This should correctly handle the ".opt", ".byte", ".exe" situations.
If the replacement fails, we default to "coqtop", hoping it's somewhere
- in the path. Note that the -coqtop option to coqide allows to override
+ in the path. Note that the -coqtop option to coqide overrides
this default coqtop path *)
let read_coqide_args argv =