diff options
| author | David Aspinall | 2002-09-11 21:44:23 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-09-11 21:44:23 +0000 |
| commit | 61f2c86cb46ed6273fff026ab63aa2697c74fba7 (patch) | |
| tree | f817acc6701407d1eb83ec204dd700bb641b5b8b | |
| parent | 9987452c8fd60df222142edddde6f3b6e6045255 (diff) | |
Fix typo.
| -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 |