aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar
diff options
context:
space:
mode:
authorGravatar Makarius Wenzel <makarius@sketis.net>2007-09-07 20:10:53 +0000
committerGravatar Makarius Wenzel <makarius@sketis.net>2007-09-07 20:10:53 +0000
commit48d434ad92c8bf0d1fb4bdf39bcca892ec7e4041 (patch)
tree7649b2db4bb8daf0f8135385dc6fbc0c3557b2f5 /isar
parent129a75d56a9a284bdff365177c6fb4db2c385fce (diff)
allow more specials: oct 327 .. oct 340;
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 a1a73731..b13c5275 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -223,7 +223,7 @@ See -k option for Isabelle interface script."
;; should be: "[\350-\377]\\|\^A[A-Z]", but literal chars
;; prevent problems with XEmacs 21.5 (beta)
- "è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ\\|[A-Z]"
+ "×\\|Ø\\|Ù\\|Ú\\|Û\\|Ü\\|Ý\\|Þ\\|ß\\|8\\|è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ\\|[0-9A-Z]"
pg-after-fontify-output-hook 'pg-remove-specials
pg-subterm-help-cmd "term %s"