| changeset 2946 | 3178e9a44d3c |
| parent 2941 | b228efa26ea3 |
| child 2966 | 09e87e779b7d |
| 2945:b4f3840a42f8 | 2946:3178e9a44d3c |
|---|---|
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("src/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); |