diff options
| -rw-r--r-- | generic/pg-goals.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 5b2e88de..45a3b8a0 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -105,7 +105,7 @@ and properly fontifies STRING using proof-fontify-region." (erase-buffer) ;; Only bother processing and displaying, etc, if string is ;; non-empty. - (unless (string-equals string "") + (unless (string-equal string "") (insert string) (if pg-use-specials-for-fontify |