aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2003-06-08 21:07:41 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2003-06-08 21:07:41 +0000
commit2c6e3b95b7d9669885129c06112ef608e5cb616a (patch)
treed5e747a36f43c4fdcac8e324e1babf320e6738f9 /generic
parent2bf1e7cf36499ceedd8b83fd97aa502623f4b622 (diff)
Robustness in pg-identifier-under-mouse-query.
Diffstat (limited to 'generic')
-rw-r--r--generic/pg-user.el8
1 files changed, 5 insertions, 3 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 56bd2970..4351a8b3 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1048,9 +1048,11 @@ The function `substitute-command-keys' is called on the argument."
(save-excursion
(mouse-set-point event)
(current-word))))))
- (proof-shell-invisible-command
- (format proof-shell-identifier-under-mouse-cmd
- identifier)))))
+ (unless (or (null identifier)
+ (string-equal identifier ""))
+ (proof-shell-invisible-command
+ (format proof-shell-identifier-under-mouse-cmd
+ identifier))))))