# HG changeset patch
# User wenzelm
# Date 1495892902 -7200
# Node ID 34c4cd9abc1a5df906833673074f967968e379f3
# Parent  453cf5c943451c26bee33118256a787e0cb8e0aa
no exit code from build processes by default, e.g. relevant for non-strict results of remote_build_history;

diff -r 453cf5c94345 -r 34c4cd9abc1a src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat May 27 13:24:01 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat May 27 15:48:22 2017 +0200
@@ -332,6 +332,7 @@
       var rev = default_rev
       var build_tags = List.empty[String]
       var verbose = false
+      var exit_code = false
 
       val getopts = Getopts("""
 Usage: isabelle build_history [OPTIONS] REPOSITORY [ARGS ...]
@@ -353,6 +354,7 @@
     -r REV       update to revision (default: """ + default_rev + """)
     -t TAG       free-form build tag (multiple occurrences possible)
     -v           verbose
+    -x           return overall exit code from build processes
 
   Build Isabelle sessions from the history of another REPOSITORY clone,
   passing ARGS directly to its isabelle build tool.
@@ -379,7 +381,8 @@
         "o:" -> (arg => output_file = arg),
         "r:" -> (arg => rev = arg),
         "t:" -> (arg => build_tags = build_tags ::: List(arg)),
-        "v" -> (_ => verbose = true))
+        "v" -> (_ => verbose = true),
+        "x" -> (_ => exit_code = true))
 
       val more_args = getopts(args)
       val (root, build_args) =
@@ -409,7 +412,7 @@
       }
 
       val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
-      if (rc != 0) sys.exit(rc)
+      if (rc != 0 && exit_code) sys.exit(rc)
     }
   }