diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2012-10-30 21:15:04 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2012-10-30 21:15:04 +0000 |
| commit | 5428910bc564b907d0f04d201154c0f214178d8a (patch) | |
| tree | b16b969e8f9823d871a11d1c0c2442f090447160 /coq/coq-seq-compile.el | |
| parent | 8ede5e10c147191822653afc0a4e2e5a53749833 (diff) | |
move some more material into coq-compile-common
Diffstat (limited to 'coq/coq-seq-compile.el')
| -rw-r--r-- | coq/coq-seq-compile.el | 16 |
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) |