aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2012-08-31 11:15:17 +0000
committerPierre Courtieu2012-08-31 11:15:17 +0000
commit35e2869eb2cf86f34152d49bb611e1b6ea941ade (patch)
tree251afa1c2c36980d128e8e2145bdc9525e054f4c
parentc97b951891a18b988816effba50612e4e9644f15 (diff)
Resize response window when showing an ancient goal.
-rw-r--r--coq/coq.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/coq/coq.el b/coq/coq.el
index d00ceb4c..252d8458 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -884,7 +884,8 @@ flag Printing All set."
(set-buffer proof-response-buffer)
(let ((inhibit-read-only 'titi))
(pg-response-display s)
- (proof-display-and-keep-buffer proof-response-buffer))))
+ (proof-display-and-keep-buffer proof-response-buffer)
+ (coq-optimise-resp-windows))))
(if withprintingall
(coq-ask-do-show-all "Show goal number" "Show" t)
(coq-ask-do "Show goal number" "Show" t))))