--- a/Admin/fixencoding Sat Mar 07 16:29:29 1998 +0100
+++ b/Admin/fixencoding Mon Mar 09 16:05:34 1998 +0100
@@ -123,7 +123,7 @@
# make tables
for ($current = $enc_first; $current <= $enc_last; $current++) {
- push(@ml_tab, '"' . $enc_tab[$current] . '"');
+ push(@ml_tab, '"\\\\<' . $enc_tab[$current] . '>"');
push(@perl_tab, sprintf('"\\x%2x", "\\\\<%s>"', $current, $enc_tab[$current]));
push(@perl_revtab, sprintf('"\\\\<%s>", "\\x%2x"', $enc_tab[$current], $current));
}
@@ -135,7 +135,7 @@
# patch files
-&patch_file("Pure/Syntax/symbol_font.ML", $ml_tab);
+&patch_file("Pure/Syntax/symbol.ML", $ml_tab);
&patch_file("Distribution/lib/scripts/symbolinput.pl", $perl_tab);
&patch_file("Distribution/lib/scripts/feeder.pl", $perl_tab);
#&patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab);