diff options
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)) |