diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2002-09-11 21:44:23 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2002-09-11 21:44:23 +0000 |
commit | 61f2c86cb46ed6273fff026ab63aa2697c74fba7 (patch) | |
tree | f817acc6701407d1eb83ec204dd700bb641b5b8b /generic/pg-goals.el | |
parent | 9987452c8fd60df222142edddde6f3b6e6045255 (diff) |
Fix typo.
Diffstat (limited to 'generic/pg-goals.el')
-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 |