diff -r d06c44532706 -r 89269bb8e7ca src/Pure/Tools/keywords.scala --- 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)) } }