equal
deleted
inserted
replaced
139 |
139 |
140 out.toString |
140 out.toString |
141 } |
141 } |
142 |
142 |
143 val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el" |
143 val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el" |
144 System.err.println(file) |
144 Output.writeln(file) |
145 File.write(Path.explode(file), output) |
145 File.write(Path.explode(file), output) |
146 } |
146 } |
147 |
147 |
148 |
148 |
149 /* administrative update_keywords */ |
149 /* administrative update_keywords */ |