diff options
author | Makarius Wenzel <makarius@sketis.net> | 2000-06-03 22:12:32 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2000-06-03 22:12:32 +0000 |
commit | 70f99119285a02089b32c54c758e2d8a59680a71 (patch) | |
tree | 01ad892e9bf44087d065a299d2d21da3fd132e55 /isar/isar-keywords.el | |
parent | 412c63386bab6e2be010ae02c6017561e56bc591 (diff) |
{ } are back;
Diffstat (limited to 'isar/isar-keywords.el')
-rw-r--r-- | isar/isar-keywords.el | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el index 520ad80f..f2d180a1 100644 --- a/isar/isar-keywords.el +++ b/isar/isar-keywords.el @@ -149,11 +149,8 @@ "use_thy_only" "welcome" "with" - ;; FIXME da: commented out these since {* *} appear after start of - ;; command, e.g. header {* blah *} etc, which breaks - ;; proof-script-command-start-regexp - ;; "{" - ;; "}" + "{" + "}" )) (defconst isar-keywords-minor |