src/Pure/Tools/keywords.scala
changeset 56631 89269bb8e7ca
parent 56146 8453d35e4684
child 56830 e760242101fc
--- 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))
       }
     }