diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-03-03 09:36:22 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-03-03 09:36:22 +0000 |
| commit | 3c071eb4457c077286049f03d0bc8f025d497281 (patch) | |
| tree | b35c7790c4f56a5286607c9bbee7ede1bc9621dd /coq/coq-compile-common.el | |
| parent | 17185897996db7c001b9c5c1e0cbef8860388e07 (diff) | |
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.
Diffstat (limited to 'coq/coq-compile-common.el')
| -rw-r--r-- | coq/coq-compile-common.el | 8 |
1 files changed, 4 insertions, 4 deletions
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) |