diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2002-06-08 10:25:42 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2002-06-08 10:25:42 +0000 |
commit | 524d4d817eb5549cfb453afd3a6222245741177c (patch) | |
tree | 3e67574de0899430b5e8beadd61991513bdae3c0 /isar | |
parent | 3be2b1fb7fa1e7a0df9369efb96c7e79df31de2c (diff) |
Fix bug in string syntax in isar-strip-terminators: did this work correctly before?
Diffstat (limited to 'isar')
-rw-r--r-- | isar/isar.el | 3 |
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) |