aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.ml
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-21 17:53:50 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-22 17:13:32 +0200
commit4271bebb68b09ddcc0d283ab16acaab399e22f13 (patch)
treeb05c67fa3b5283775f9ea39b7d8fb492de036b41 /ide/ideutils.ml
parent9055359520294ac1089934eb41e1b3b2fe0987a1 (diff)
Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file exists
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r--ide/ideutils.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 32d2bb97b..424c41a60 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -249,7 +249,7 @@ let coqtop_path () =
let i = Str.search_backward (Str.regexp_string "coqide") prog pos
in
String.blit "coqtop" 0 prog i 6;
- prog
+ if Sys.file_exists prog then prog else "coqtop"
with Not_found -> "coqtop"
in file