diff options
author | 2004-02-18 16:59:29 +0000 | |
---|---|---|
committer | 2004-02-18 16:59:29 +0000 | |
commit | 8a50e54695813d47a6492624993300beccd7913d (patch) | |
tree | 737a1e2116a38e59020bfc53c0cfa356e1f6b884 /generic/pg-user.el | |
parent | 975fd24a2b189834110d75b30b985cda6892db8b (diff) |
holes implementation, it uses span.el. mouse keybindings work
correctly for xemacs (any version) and emacs > 21.
Diffstat (limited to 'generic/pg-user.el')
-rw-r--r-- | generic/pg-user.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 0e423d1d..bc2effba 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1036,9 +1036,9 @@ The function `substitute-command-keys' is called on the argument." ;; this modifier combination is currently unused. (cond (proof-running-on-Emacs21 - (global-set-key [C-M-mouse-1] 'pg-identifier-under-mouse-query)) + (global-set-key [C-M-mouse-2] 'pg-identifier-under-mouse-query)) (proof-running-on-XEmacs - (global-set-key '(control meta button1) 'pg-identifier-under-mouse-query))) + (global-set-key '(control meta button2) 'pg-identifier-under-mouse-query))) (defun pg-identifier-under-mouse-query (event) (interactive "e") |