aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2016-04-25 18:17:45 -0400
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2016-04-25 18:17:45 -0400
commit1c4fd3f01116ace158d3885e8a11c29f71d19823 (patch)
tree0676df6621b040064275db6f6b08d4dd9c51c8e7 /coq/coq.el
parent324ba527662580cfabc3db07d63f30f6515f2aab (diff)
Don't use string-empty-p
It's too recent
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 49d72c16..a75760ed 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2055,7 +2055,7 @@ mouse activation."
(defun coq--format-intros (output)
"Create an “intros” form from the OUTPUT of “Show Intros”."
(let* ((shints (replace-regexp-in-string "[\r\n ]*\\'" "" output)))
- (if (or (string-empty-p shints)
+ (if (or (string= "" shints)
(string-match coq-error-regexp shints))
(error "Don't know what to intro")
(format "intros %s" shints))))