diff options
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)))))) |