diff options
author | 2003-06-08 21:07:41 +0000 | |
---|---|---|
committer | 2003-06-08 21:07:41 +0000 | |
commit | 2c6e3b95b7d9669885129c06112ef608e5cb616a (patch) | |
tree | d5e747a36f43c4fdcac8e324e1babf320e6738f9 /generic | |
parent | 2bf1e7cf36499ceedd8b83fd97aa502623f4b622 (diff) |
Robustness in pg-identifier-under-mouse-query.
Diffstat (limited to 'generic')
-rw-r--r-- | generic/pg-user.el | 8 |
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)))))) |