From 7aafefd252df6ff13b93ad388e767c771f56e916 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 12 Dec 2016 11:27:24 +0100
Subject: remove default absolute name from coq-prog-name, but keep dipsplaying
 it when asking for it.

---
 coq/coq-system.el      | 3 ++-
 generic/proof-shell.el | 6 ++++--
 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)))
 
-- 
cgit v1.2.3