aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--BUGS1
-rw-r--r--generic/proof-script.el14
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)))