Added proof-terminal-string to proof-execute-minibuffer-cmd.

2 files changed, 10 insertions, 5 deletions

diff --git a/BUGS b/BUGS
index cfb89879..d6e8c577 100644
--- a/BUGS
+++ b/BUGS
@@ -89,7 +89,6 @@ interrupt, the whole process may be killed instead of interrupted.
 This isn't a bug in Proof General, but the behaviour of ssh.  Try
 using rsh instead, it is said to forward signals to the remote command.
 
-
 FSF Emacs specific bugs
 =======================
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 556b2f22..af881c23 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1342,7 +1342,10 @@ even more dangerous than proof-try-command."
     ;; (proof-shell-ready-prover)
     ;; was (proof-check-process-available 'relaxed) 
     (setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
-    (proof-shell-invisible-command cmd)))
+    (proof-shell-invisible-command 
+     (if proof-terminal-string
+	 (concat cmd proof-terminal-string)
+       cmd))))
 
 
 
@@ -1395,17 +1398,20 @@ even more dangerous than proof-try-command."
 (defun proof-ctxt ()
   "List context."
   (interactive) 
-  (proof-shell-invisible-command (concat proof-ctxt-string proof-terminal-string)))
+  (proof-shell-invisible-command 
+   (concat proof-ctxt-string proof-terminal-string)))
 
 (defun proof-help ()
   "Print help message giving syntax."
   (interactive)
-  (proof-shell-invisible-command (concat proof-help-string proof-terminal-string)))
+  (proof-shell-invisible-command 
+   (concat proof-help-string proof-terminal-string)))
 
 (defun proof-prf ()
   "List proof state."
   (interactive)
-  (proof-shell-invisible-command (concat proof-prf-string proof-terminal-string)))
+  (proof-shell-invisible-command
+   (concat proof-prf-string proof-terminal-string)))