src/Pure/Tools/build.scala
changeset 65281 c70e7d24a16d
parent 65278 b553d0edc440
child 65282 f4c5f10829a0
--- a/src/Pure/Tools/build.scala	Thu Mar 16 23:27:29 2017 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 16 23:33:39 2017 +0100
@@ -203,6 +203,9 @@
 
   /* sources and heaps */
 
+  sealed case class Session_Info(
+    sources: String, input_heap: String, output_heap: String, return_code: Int)
+
   private val SOURCES = "sources: "
   private val INPUT_HEAP = "input_heap: "
   private val OUTPUT_HEAP = "output_heap: "