diff options
| author | David Aspinall | 2003-06-08 21:07:41 +0000 |
|---|---|---|
| committer | David Aspinall | 2003-06-08 21:07:41 +0000 |
| commit | 2c6e3b95b7d9669885129c06112ef608e5cb616a (patch) | |
| tree | d5e747a36f43c4fdcac8e324e1babf320e6738f9 | |
| parent | 2bf1e7cf36499ceedd8b83fd97aa502623f4b622 (diff) | |
Robustness in pg-identifier-under-mouse-query.
| -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)))))) |