Opened 14 years ago
Closed 14 years ago
#365 closed defect (fixed)
Fix three mouse bindings in proof-menu.el, pg-goals.el, and pg-vars.el
| Reported by: | Erik Martin-Dorel | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.0 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | Erik Martin-Dorel |
Description
The "mouse bindings" associated with proof-mouse-goto-point,
proof-undo-and-delete-last-successful-command in *goals*, and
pg-identifier-under-mouse-query needed to be fixed to avoid
conflicts with existing GNU Emacs or PG bindings, including the one
for holes-mouse-set-make-active-hole that was more or less
overwritten.
I will upload a patch that should make these functions fully functional.
Kind regards, Erik Martin-Dorel.
Attachments (1)
Change History (2)
Changed 14 years ago by
| Attachment: | mouse-bindings.patch added |
|---|
comment:1 Changed 14 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
Patch applied, many thanks!
Note: See
TracTickets for help on using
tickets.
Patch for generic/{proof-menu,pg-goals,pg-vars}.el