src/Pure/Tools/build.scala
changeset 66747 f4c6c8a8f645
parent 66746 888a51e77c6e
child 66749 0445cfaf6132
     1.1 --- a/src/Pure/Tools/build.scala	Mon Oct 02 13:33:36 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 02 13:40:51 2017 +0200
     1.3 @@ -28,6 +28,9 @@
     1.4      input_heaps: List[String],
     1.5      output_heap: Option[String],
     1.6      return_code: Int)
     1.7 +  {
     1.8 +    def ok: Boolean = return_code == 0
     1.9 +  }
    1.10  
    1.11  
    1.12    /* queue with scheduling information */
    1.13 @@ -397,8 +400,7 @@
    1.14                case Some(database) =>
    1.15                  using(SQLite.open_database(database))(store.read_build(_, name)) match {
    1.16                    case Some(build)
    1.17 -                  if build.return_code == 0 &&
    1.18 -                    build.sources == sources_stamp(deps0, name) => None
    1.19 +                  if build.ok && build.sources == sources_stamp(deps0, name) => None
    1.20                    case _ => Some(name)
    1.21                  }
    1.22                case None => Some(name)
    1.23 @@ -566,7 +568,7 @@
    1.24                        using(SQLite.open_database(database))(store.read_build(_, name)) match {
    1.25                          case Some(build) =>
    1.26                            val current =
    1.27 -                            build.return_code == 0 &&
    1.28 +                            build.ok &&
    1.29                              build.sources == sources_stamp(deps, name) &&
    1.30                              build.input_heaps == ancestor_heaps &&
    1.31                              build.output_heap == heap_stamp &&