From 2c6e3b95b7d9669885129c06112ef608e5cb616a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 8 Jun 2003 21:07:41 +0000 Subject: Robustness in pg-identifier-under-mouse-query. --- generic/pg-user.el | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'generic') 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)))))) -- cgit v1.2.3