From 3c071eb4457c077286049f03d0bc8f025d497281 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 3 Mar 2015 09:36:22 +0000 Subject: Coqtop always restarted when switching script buffer. This comes from Hendrik's compile mode and is actually needed even when this mode is off. When switching scripting buffer, restart the coq shell process, so that it applies local coqtop options. --- coq/coq-compile-common.el | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'coq/coq-compile-common.el') diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 5a8c3af0..0f7c82af 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -654,10 +654,10 @@ correct in the new scripting buffer." (unless proof-shell-exit-in-progress (proof-shell-exit t))) - -(add-hook 'proof-deactivate-scripting-hook - 'coq-switch-buffer-kill-proof-shell - t) +;; This is now always done (in coq.el) +;(add-hook 'proof-deactivate-scripting-hook +; 'coq-switch-buffer-kill-proof-shell +; t) (provide 'coq-compile-common) -- cgit v1.2.3