aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-user.el
diff options
context:
space:
mode:
Diffstat (limited to 'generic/pg-user.el')
-rw-r--r--generic/pg-user.el7
1 files changed, 5 insertions, 2 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 2c490569..c439e995 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1023,8 +1023,11 @@ If NUM is negative, move upwards. Return new span."
(defun pg-response-buffers-hint (&optional nextbuf)
(pg-hint
(format
- "Use \\[proof-prf] to display goals; \\[proof-display-some-buffers] to rotate output %s"
- (if nextbuf (concat "(next: " nextbuf ")") ""))))
+ "\\[proof-prf] displays goals;%s \\[proof-layout-windows] refreshes"
+ (if (not proof-multiple-frames-enable) ;; and not proof-three-window-enable?
+ (format " \\[proof-display-some-buffers] rotates output%s;"
+ (if nextbuf (concat " (next:" nextbuf ")") ""))
+ ""))))
(defun pg-jump-to-end-hint ()
(pg-hint "Use \\[proof-goto-end-of-locked] to jump to end of processed region"))