| changeset 4500 | db49bac6256a |
| parent 4499 | 4ca67338e22c |
| child 4687 | 8cec457a8961 |
--- 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);