| changeset 2423 | 4550426cf8f7 |
| parent 2397 | 01a5e30334b1 |
| child 2424 | a310d0c89789 |
--- a/lib/scripts/symbolinput.pl Mon Dec 16 15:45:01 1996 +0100 +++ b/lib/scripts/symbolinput.pl Mon Dec 16 15:45:02 1996 +0100 @@ -4,6 +4,7 @@ # Copyright 1996 Technische Universitaet Muenchen # # translate symbols into \<...> sequences. +# table must be consistent with Pure/Syntax/symbol_font.ML %tab = ( "\xa1", "\\\\<Gamma>",