aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/pg-user.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-10-17 09:51:26 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-10-17 09:51:26 +0000
commit9e1ad692f7dc96e8c2f0475de7dc2b5629e9e690 (patch)
treee10aab524eb75f642ef073e1059f34ca8b9ab8c0 /generic/pg-user.el
parent0be7f2bf48f81c215e4861cdb201e5c233438d7e (diff)
Remove dependency of pg-movie on pg-user
Diffstat (limited to 'generic/pg-user.el')
-rw-r--r--generic/pg-user.el1
1 files changed, 1 insertions, 0 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 37d16175..e08d7f0c 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -192,6 +192,7 @@ If inside a comment, just process until the start of the comment."
(interactive)
(proof-assert-until-point))
+;;;###autoload
(defun proof-process-buffer ()
"Process the current (or script) buffer, and maybe move point to the end."
(interactive)