equal
deleted
inserted
replaced
136 # patch files |
136 # patch files |
137 |
137 |
138 &patch_file("Pure/Syntax/symbol_font.ML", $ml_tab); |
138 &patch_file("Pure/Syntax/symbol_font.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); |