diff options
| -rw-r--r-- | generic/pg-user.el | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index a8768812..e49dcba5 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -706,6 +706,7 @@ If NUM is negative, move upwards. Return new span." (span-at (pg-pos-for-event event) 'type)) (defun pg-span-context-menu (event) + "Display a context sensitive menu for proof script, around EVENT." (interactive "e") (let* ((span (pg-span-for-event event)) cspan) |