aboutsummaryrefslogtreecommitdiff
path: root/hol-light/hol-light.el
diff options
context:
space:
mode:
authorDavid Aspinall2012-02-08 18:00:57 +0000
committerDavid Aspinall2012-02-08 18:00:57 +0000
commitb794252aab2673cc60ecbfcc8fe8bf454e5468ea (patch)
treea255cf77a33ed2481c1e8e0fcc1a2f30dd4c1895 /hol-light/hol-light.el
parentaf00bfad9b14dd182259d376f11ad7af046d4444 (diff)
Abort attempt to use special exception printing
Diffstat (limited to 'hol-light/hol-light.el')
-rw-r--r--hol-light/hol-light.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el
index 4b366f6c..18192ed1 100644
--- a/hol-light/hol-light.el
+++ b/hol-light/hol-light.el
@@ -114,7 +114,7 @@ You need to restart Emacs if you change this setting."
"Value for `proof-shell-error-regexp' with standard top level.")
(defconst hol-light-annotated-error-regexp
- ;; "<error>.+</error>" ;; FIXME: include new lines, also fix pg_prompt.ml
+ ;; "<error>.+</error>" ;; unfortunately not enough, this is only for failwith
hol-light-plain-error-regexp
"Value for `proof-shell-error-regexp' with custom top level.")