aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-seq-compile.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq-seq-compile.el')
-rw-r--r--coq/coq-seq-compile.el16
1 files changed, 0 insertions, 16 deletions
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index d7b50f8c..7e9e0bfd 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -502,22 +502,6 @@ compilation (if necessary) of the dependencies."
(add-hook 'proof-shell-extend-queue-hook 'coq-preprocess-require-commands)
-;; kill coqtop on script buffer change
-
-(defun coq-switch-buffer-kill-proof-shell ()
- "Kill the proof shell without asking the user.
-This function is for `proof-deactivate-scripting-hook'. It kills
-the proof shell without asking the user for
-confirmation (assuming she agreed already on switching the active
-scripting buffer). This is needed to ensure the load path is
-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)