diff options
| author | David Aspinall | 2000-06-09 19:08:19 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-06-09 19:08:19 +0000 |
| commit | af052e58725ed56729ac63cda3aaa902cc8d1852 (patch) | |
| tree | ce33154007a2e1ae3bec837c7bfb2e8a1563a709 /generic | |
| parent | c6c47960411f80cb60019345c1f852b331c8a8bb (diff) | |
Comment
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 48ee05af..486ccef9 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2555,7 +2555,7 @@ Clean up before a script buffer is killed. If killing the active scripting buffer, run proof-deactivate-scripting. Otherwise just do proof-restart-buffers to delete some spans from memory." ;; Deactivate scripting in the current buffer if need be, forcing - ;; retraction. + ;; automatic retraction if the buffer is not fully processed. (unwind-protect (if (eq (current-buffer) proof-script-buffer) (proof-deactivate-scripting 'retract)) |