aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2001-12-05 15:34:20 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2001-12-05 15:34:20 +0000
commit990f07fb23220c8294c1090e6d44bd0c5a7dda18 (patch)
tree16bd201ce9463f629f413130ac99f2fa8eb4beb9 /isar
parent15bcb360c5948b241c3a24c72eabcea862f99f4c (diff)
activate proof-shell-spill-output-regexp;
Diffstat (limited to 'isar')
-rw-r--r--isar/isar.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/isar/isar.el b/isar/isar.el
index db70761d..bc487727 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -206,7 +206,7 @@
proof-shell-eager-annotation-start-length 1
proof-shell-eager-annotation-start "\360\\|\362"
proof-shell-eager-annotation-end "\361\\|\363"
-; proof-shell-spill-output-regexp "\375"
+ proof-shell-spill-output-regexp "\375"
;; Some messages delimited by eager annotations
proof-shell-clear-response-regexp "Proof General, please clear the response buffer."