--- a/src/Pure/Tools/build.scala Sat Nov 11 18:41:08 2017 +0000
+++ b/src/Pure/Tools/build.scala Sun Nov 12 12:41:05 2017 +0100
@@ -71,7 +71,7 @@
}
}
- def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
+ def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
{
val graph = sessions.build_graph
val names = graph.keys
@@ -178,7 +178,7 @@
private class Job(progress: Progress,
name: String,
val info: Sessions.Info,
- sessions: Sessions.T,
+ sessions: Sessions.Structure,
deps: Sessions.Deps,
store: Sessions.Store,
do_output: Boolean,