aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-27 11:28:07 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-27 11:28:07 +0000
commit39cb0b047ea9d2fd362dc2e1e1cce6a72857890d (patch)
treec7102d533066f6953b81cff2316e5f266a13ec0d /generic
parent3d71d5570534b75abd63b2ec74efc28e60f1c2b7 (diff)
Disable undo history for efficiency.
Diffstat (limited to 'generic')
-rw-r--r--generic/pg-goals.el4
1 files changed, 3 insertions, 1 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 2e98fd73..907f4fe5 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -32,7 +32,9 @@ May enable proof-by-pointing or similar features.
(easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
(easy-menu-add proof-assistant-menu proof-goals-mode-map)
(proof-toolbar-setup)
- (erase-buffer)))
+ (erase-buffer)
+ (buffer-disable-undo)
+ (set-buffer-modified-p nil)))
;;
;; Keys for goals buffer