# HG changeset patch
# User wenzelm
# Date 1398162654 -7200
# Node ID 89269bb8e7ca1cc24892445e5f9717fb2880761e
# Parent  d06c44532706e60147fc25df6d71900ed7e5e4ea
tuned;

diff -r d06c44532706 -r 89269bb8e7ca src/Pure/System/command_line.scala
--- 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 }
 }
 
diff -r d06c44532706 -r 89269bb8e7ca src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/System/options.scala	Tue Apr 22 12:30:54 2014 +0200
@@ -141,7 +141,7 @@
 
   def main(args: Array[String])
   {
-    Command_Line.tool {
+    Command_Line.tool0 {
       args.toList match {
         case get_option :: export_file :: more_options =>
           val options = (Options.init() /: more_options)(_ + _)
@@ -155,7 +155,6 @@
           if (get_option == "" && export_file == "")
             System.out.println(options.print)
 
-          0
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }
diff -r d06c44532706 -r 89269bb8e7ca src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Apr 22 12:05:02 2014 +0200
+++ b/src/Pure/Tools/build.ML	Tue Apr 22 12:30:54 2014 +0200
@@ -124,7 +124,7 @@
 
 in
 
-fun build args_file = Command_Line.tool (fn () =>
+fun build args_file = Command_Line.tool0 (fn () =>
     let
       val _ = SHA1_Samples.test ();
 
@@ -167,7 +167,7 @@
 
       val _ = Options.reset_default ();
       val _ = if do_output then () else exit 0;
-    in 0 end);
+    in () end);
 
 end;
 
diff -r d06c44532706 -r 89269bb8e7ca src/Pure/Tools/doc.scala
--- 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
     }
   }
 }
diff -r d06c44532706 -r 89269bb8e7ca src/Pure/Tools/keywords.scala
--- 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))
       }
     }