src/Pure/Tools/doc.scala
changeset 56631 89269bb8e7ca
parent 56425 d12653fbd5b1
child 56784 776890e0cf71
--- a/src/Pure/Tools/doc.scala	Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/Tools/doc.scala	Tue Apr 22 12:30:54 2014 +0200
@@ -90,7 +90,7 @@
 
   def main(args: Array[String])
   {
-    Command_Line.tool {
+    Command_Line.tool0 {
       val entries = contents()
       if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
       else {
@@ -101,7 +101,6 @@
           }
         )
       }
-      0
     }
   }
 }