| changeset 4499 | 4ca67338e22c |
| parent 2966 | 09e87e779b7d |
| child 4500 | db49bac6256a |
| 4498:a088ec3e4f5e | 4499:4ca67338e22c |
|---|---|
135 |
135 |
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); |
|
141 &patch_file("Distribution/lib/scripts/symboloutput.pl", $perl_revtab); |