src/Pure/System/command_line.scala
changeset 56631 89269bb8e7ca
parent 55618 995162143ef4
child 56669 f42717b5dc84
--- a/src/Pure/System/command_line.scala	Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/System/command_line.scala	Tue Apr 22 12:30:54 2014 +0200
@@ -35,5 +35,7 @@
       }
     sys.exit(rc)
   }
+
+  def tool0(body: => Unit): Nothing = tool { body; 0 }
 }