equal
deleted
inserted
replaced
162 |
162 |
163 /* command line entry point */ |
163 /* command line entry point */ |
164 |
164 |
165 def main(args: Array[String]) |
165 def main(args: Array[String]) |
166 { |
166 { |
167 Command_Line.tool { |
167 Command_Line.tool0 { |
168 args.toList match { |
168 args.toList match { |
169 case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) => |
169 case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) => |
170 keywords(Options.init(), name, dirs.map(Path.explode), sessions) |
170 keywords(Options.init(), name, dirs.map(Path.explode), sessions) |
171 0 |
|
172 case "update_keywords" :: Nil => |
171 case "update_keywords" :: Nil => |
173 update_keywords(Options.init()) |
172 update_keywords(Options.init()) |
174 0 |
|
175 case _ => error("Bad arguments:\n" + cat_lines(args)) |
173 case _ => error("Bad arguments:\n" + cat_lines(args)) |
176 } |
174 } |
177 } |
175 } |
178 } |
176 } |
179 } |
177 } |