diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-11-30 23:44:54 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-11-30 23:44:54 +0000 |
| commit | 7e3eb90d09027bc29a6d592769dad562b1e02855 (patch) | |
| tree | 938ea04b467a18ab38b82e3bf4a39d0791e4e638 | |
| parent | 2fafa16d69106aac0338b96e2a8db894d93764e9 (diff) | |
Fix for Trac #307.
| -rw-r--r-- | generic/proof-script.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 66d101fc..b2c71bce 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1129,13 +1129,13 @@ activation is considered to have failed and an error is given." (unless (eq proof-buffer-type 'script) (error "Must be running in a script buffer!")) + (proof-shell-ready-prover queuemode) ; fire up/check mode + (unless (equal (current-buffer) proof-script-buffer) ;; TODO: narrow the scope of this save-excursion. ;; Where is it needed? Maybe hook functions. (save-excursion - (proof-shell-ready-prover queuemode) ; fire up the prover - ;; If there's another buffer currently active, we need to ;; deactivate it (also fixing up the included files list). (if proof-script-buffer |