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 } } }