diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-user.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 7e8aa173..0e423d1d 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1037,7 +1037,7 @@ The function `substitute-command-keys' is called on the argument." (cond (proof-running-on-Emacs21 (global-set-key [C-M-mouse-1] 'pg-identifier-under-mouse-query)) - (proof-running-on-Xemacs + (proof-running-on-XEmacs (global-set-key '(control meta button1) 'pg-identifier-under-mouse-query))) (defun pg-identifier-under-mouse-query (event) |