src/Pure/Tools/build.scala
changeset 66594 c16ed3250de0
parent 66571 0fdeb24e535e
child 66595 fa10b0f589c3
     1.1 --- a/src/Pure/Tools/build.scala	Fri Sep 01 15:42:10 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Sep 02 12:09:07 2017 +0200
     1.3 @@ -416,8 +416,10 @@
     1.4  
     1.5      // scheduler loop
     1.6      case class Result(
     1.7 -      current: Boolean, heap_stamp: Option[String],
     1.8 -      process: Option[Process_Result], info: Sessions.Info)
     1.9 +      current: Boolean,
    1.10 +      heap_stamp: Option[String],
    1.11 +      process: Option[Process_Result],
    1.12 +      info: Sessions.Info)
    1.13      {
    1.14        def ok: Boolean =
    1.15          process match {