aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--coq/coq-system.el3
-rw-r--r--generic/proof-shell.el6
2 files changed, 6 insertions, 3 deletions
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 997e93d2..5d9df691 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -30,7 +30,8 @@ On Windows you might need something like:
:group 'coq)
(defcustom coq-prog-name
- (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin"))
+ (if (executable-find "coqtop") "coqtop"
+ (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin")))
"*Name of program to run as Coq. See `proof-prog-name', set from this.
On Windows with latest Coq package you might need something like:
C:/Program Files/Coq/bin/coqtop.opt.exe
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 64eee4c8..7b19fded 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -293,8 +293,10 @@ process command."
(apply proof-guess-command-line (list name)))))
(if proof-prog-name-ask
- (setq proof-prog-name (read-shell-command "Run process: "
- proof-prog-name)))
+ ;; if this option is set, an absolute file name is better to show if possible
+ (let ((prog-name (locate-file proof-prog-name exec-path exec-suffixes 1)))
+ (setq proof-prog-name (read-shell-command "Run process: "
+ prog-name))))
(let
((proc (downcase proof-assistant)))