author | wenzelm |
Mon, 29 Dec 1997 21:38:19 +0100 | |
changeset 4500 | db49bac6256a |
parent 4499 | 4ca67338e22c |
child 4501 | 5f629ee2502b |
Admin/fixencoding | file | annotate | diff | comparison | revisions |
--- a/Admin/fixencoding Mon Dec 29 21:37:23 1997 +0100 +++ b/Admin/fixencoding Mon Dec 29 21:38:19 1997 +0100 @@ -138,4 +138,4 @@ &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); +#&patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab);