author | wenzelm |
Mon, 29 Dec 1997 21:37:23 +0100 | |
changeset 4499 | 4ca67338e22c |
parent 4498 | a088ec3e4f5e |
child 4500 | db49bac6256a |
Admin/fixencoding | file | annotate | diff | comparison | revisions |
--- 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);