src/Pure/Thy/sessions.scala
changeset 66749 0445cfaf6132
parent 66746 888a51e77c6e
child 66759 918f15c9367a
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 02 13:45:36 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 02 15:37:46 2017 +0200
     1.3 @@ -908,7 +908,7 @@
     1.4            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
     1.5            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
     1.6            stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
     1.7 -          stmt.string(7) = cat_lines(build.sources)
     1.8 +          stmt.string(7) = build.sources
     1.9            stmt.string(8) = cat_lines(build.input_heaps)
    1.10            stmt.string(9) = build.output_heap getOrElse ""
    1.11            stmt.int(10) = build.return_code
    1.12 @@ -942,7 +942,7 @@
    1.13          else {
    1.14            Some(
    1.15              Build.Session_Info(
    1.16 -              split_lines(res.string(Session_Info.sources)),
    1.17 +              res.string(Session_Info.sources),
    1.18                split_lines(res.string(Session_Info.input_heaps)),
    1.19                res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) },
    1.20                res.int(Session_Info.return_code)))