aboutsummaryrefslogtreecommitdiff
path: root/coq
diff options
context:
space:
mode:
authorPierre Courtieu2016-01-06 17:08:57 +0100
committerPierre Courtieu2016-01-06 17:08:57 +0100
commita326ff399be1691643fe4bbbde4a27896b194e82 (patch)
treed3ecab4defbf5c52b19f11dd3ec1272adb3c17f3 /coq
parent5eff32433b3ae47d36f6acab87e7af0d273946d6 (diff)
Fixing #25.
proof-script-buffer was not set before calling proof-shell-ready-prover.
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el8
1 files changed, 2 insertions, 6 deletions
diff --git a/coq/coq.el b/coq/coq.el
index c06a7744..e83c1dbc 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2452,12 +2452,8 @@ number of hypothesis displayed, without hiding the goal"
(defun is-not-split-vertic (selected-window)
(<= (- (frame-height) (window-height)) 2))
-;; three window mode needs to be called when starting the script
-(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
-
-;; three window mode needs to be called when starting the script
-(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
-
+;; bug fixed in generic ocde, useless now:
+;(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows))))
;; *Experimental* auto shrink response buffer in three windows mode. Things get
;; a bit messed up if the response buffer is not at the right place (below