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