diff options
| author | letouzey | 2011-04-21 16:12:36 +0000 |
|---|---|---|
| committer | letouzey | 2011-04-21 16:12:36 +0000 |
| commit | eacf0de87bf18631610f0fae9af192583f27a88b (patch) | |
| tree | afa6c32c65989837c3aefd2b8eac13d26349b9f0 | |
| parent | 9ccd1899dba51e24216d0de8865eecf029f44cef (diff) | |
Coqide: better construction of default coqtop path
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14042 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ide/coqide.ml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 08c41aeaa8..a0bd8a829f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -3163,11 +3163,21 @@ let rec check_for_geoproof_input () = (* cb_Dr#set_text "Ack" *) done +(** By default, the coqtop we try to launch is exactly the current coqide + 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 + this default coqtop path *) + let default_coqtop_path () = let prog = Sys.executable_name in - let dir = Filename.dirname prog in - if Filename.check_suffix prog ".byte" then dir^"/coqtop.byte" - else dir^"/coqtop.opt" + try + let pos = String.length prog - 6 in + let i = Str.search_backward (Str.regexp_string "coqide") prog pos in + String.blit "coqtop" 0 prog i 6; + prog + with _ -> "coqtop" let set_coqtop_path argv = let coqtop = ref "" in |
