aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-06-08 10:25:42 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-06-08 10:25:42 +0000
commit524d4d817eb5549cfb453afd3a6222245741177c (patch)
tree3e67574de0899430b5e8beadd61991513bdae3c0 /isar
parent3be2b1fb7fa1e7a0df9369efb96c7e79df31de2c (diff)
Fix bug in string syntax in isar-strip-terminators: did this work correctly before?
Diffstat (limited to 'isar')
-rw-r--r--isar/isar.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/isar/isar.el b/isar/isar.el
index b7829822..4425f69b 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -94,7 +94,8 @@
(if (not (proof-buffer-syntactic-context))
(progn
(delete-backward-char 1)
- (or (proof-looking-at ";\\|\s-\\|$") (insert " ")))))))
+ (or (proof-looking-at ";\\|\\s-\\|$")
+ (insert " ")))))))
(defun isar-markup-ml (string)