--- a/src/Pure/Tools/keywords.scala Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/Tools/keywords.scala Tue Apr 22 12:30:54 2014 +0200
@@ -164,14 +164,12 @@
def main(args: Array[String])
{
- Command_Line.tool {
+ Command_Line.tool0 {
args.toList match {
case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
keywords(Options.init(), name, dirs.map(Path.explode), sessions)
- 0
case "update_keywords" :: Nil =>
update_keywords(Options.init())
- 0
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}