tuned whitespace;
authorwenzelm
Sat, 02 Sep 2017 12:09:07 +0200
changeset 66594 c16ed3250de0
parent 66593 d389714a8aaa
child 66595 fa10b0f589c3
tuned whitespace;
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Sep 01 15:42:10 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sat Sep 02 12:09:07 2017 +0200
@@ -416,8 +416,10 @@
 
     // scheduler loop
     case class Result(
-      current: Boolean, heap_stamp: Option[String],
-      process: Option[Process_Result], info: Sessions.Info)
+      current: Boolean,
+      heap_stamp: Option[String],
+      process: Option[Process_Result],
+      info: Sessions.Info)
     {
       def ok: Boolean =
         process match {