# HG changeset patch
# User wenzelm
# Date 1504346947 -7200
# Node ID c16ed3250de0b9231f087a615318a880b96fbd4d
# Parent  d389714a8aaa124bb01878ce670cd88a042c11e4
tuned whitespace;

diff -r d389714a8aaa -r c16ed3250de0 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 {