# HG changeset patch
# User wenzelm
# Date 1506944451 -7200
# Node ID f4c6c8a8f645e8d57a936b3c720c7f729728d07a
# Parent  888a51e77c6e0f5ab5583ef2101f80fbe86a1301
tuned;

diff -r 888a51e77c6e -r f4c6c8a8f645 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Oct 02 13:33:36 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Oct 02 13:40:51 2017 +0200
@@ -28,6 +28,9 @@
     input_heaps: List[String],
     output_heap: Option[String],
     return_code: Int)
+  {
+    def ok: Boolean = return_code == 0
+  }
 
 
   /* queue with scheduling information */
@@ -397,8 +400,7 @@
               case Some(database) =>
                 using(SQLite.open_database(database))(store.read_build(_, name)) match {
                   case Some(build)
-                  if build.return_code == 0 &&
-                    build.sources == sources_stamp(deps0, name) => None
+                  if build.ok && build.sources == sources_stamp(deps0, name) => None
                   case _ => Some(name)
                 }
               case None => Some(name)
@@ -566,7 +568,7 @@
                       using(SQLite.open_database(database))(store.read_build(_, name)) match {
                         case Some(build) =>
                           val current =
-                            build.return_code == 0 &&
+                            build.ok &&
                             build.sources == sources_stamp(deps, name) &&
                             build.input_heaps == ancestor_heaps &&
                             build.output_heap == heap_stamp &&