aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-goals.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-26 17:39:25 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-26 17:39:25 +0000
commitadd6299da8e4fcbb2efa16d75b9126a536cdfca5 (patch)
tree0cd39795c3f958d6dc24017e13e4c08cdab061aa /generic/pg-goals.el
parent5301fd94b22fa5e59dfcccc19e89e2f3faccd21e (diff)
Try to prevent associated buffers being killed off by user.
Diffstat (limited to 'generic/pg-goals.el')
-rw-r--r--generic/pg-goals.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 8d854ce3..2e98fd73 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -26,8 +26,9 @@
"Mode for goals display.
May enable proof-by-pointing or similar features.
\\{proof-goals-mode-map}"
- ;; defined-derived-mode proof-goals-mode initialises proof-goals-mode-map
(setq proof-buffer-type 'goals)
+ (make-local-hook 'kill-buffer-hook)
+ (add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
(easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
(easy-menu-add proof-assistant-menu proof-goals-mode-map)
(proof-toolbar-setup)