diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2002-07-16 23:11:42 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-16 23:11:42 +0000 |
commit | 0f4feea9ca0163946b2a971657b8e71c2931044d (patch) | |
tree | 8507aa084284960e2443c7ac693b8e524abb7d9f /lego/lego-syntax.el | |
parent | 4dfaa3700086d0cb6c9d8518dac894e58fa7f7a9 (diff) |
Refactor several variable names; clean up, doc subterm markup and output display.
Diffstat (limited to 'lego/lego-syntax.el')
-rw-r--r-- | lego/lego-syntax.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index e1ff82a4..bdb30a72 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -82,7 +82,7 @@ ;; Special hacks!! (cons "Discharge.." 'font-lock-keyword-face) (cons "\\*\\*\\* QED \\*\\*\\*" 'font-lock-keyword-face)) - "*Font-lock table for LEGO terms.") + "*Font-lock table for LEGO terms (displayed in output buffers).") ;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore, ;; it might be safer to append "\\s-*:". |