diff -r 49a49fc4a0f0 -r 4550426cf8f7 lib/scripts/symbolinput.pl
--- 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>",