equal
deleted
inserted
replaced
133 $perl_revtab = " " . join(",\n ", @perl_revtab) . "\n"; |
133 $perl_revtab = " " . join(",\n ", @perl_revtab) . "\n"; |
134 |
134 |
135 |
135 |
136 # patch files |
136 # patch files |
137 |
137 |
138 &patch_file("Pure/Syntax/symbol.ML", $ml_tab); |
138 &patch_file("Pure/General/symbol.ML", $ml_tab); |
139 &patch_file("Distribution/lib/scripts/symbolinput.pl", $perl_tab); |
139 &patch_file("Distribution/lib/scripts/symbolinput.pl", $perl_tab); |
140 &patch_file("Distribution/lib/scripts/feeder.pl", $perl_tab); |
140 &patch_file("Distribution/lib/scripts/feeder.pl", $perl_tab); |
141 #&patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab); |
141 #&patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab); |