src/Pure/Tools/build.scala

   sealed case class Session_Info(
     sources: List[String],
     input_heaps: List[String],
     output_heap: Option[String],
     return_code: Int)
+  {
+    def ok: Boolean = return_code == 0
+  }
 
 
   /* queue with scheduling information */
 
   private object Queue

           selected0.flatMap(name =>
             store.find_database(name) match {
               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)
             })
         val (selected, selected_sessions) =

                   store.find_database_heap(name) match {
                     case Some((database, heap_stamp)) =>
                       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 &&
                             !(do_output && heap_stamp.isEmpty)
                           (current, heap_stamp)