changeset 4499 | 4ca67338e22c |
parent 2966 | 09e87e779b7d |
child 4500 | db49bac6256a |
--- a/Admin/fixencoding Mon Dec 29 14:31:20 1997 +0100 +++ b/Admin/fixencoding Mon Dec 29 21:37:23 1997 +0100 @@ -137,3 +137,5 @@ &patch_file("Pure/Syntax/symbol_font.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);