src/Pure/Tools/build.scala
changeset 67052 caf87d4b9b61
parent 67030 a9859e879f38
child 67098 0f750a6dc754
     1.1 --- a/src/Pure/Tools/build.scala	Sat Nov 11 18:41:08 2017 +0000
     1.2 +++ b/src/Pure/Tools/build.scala	Sun Nov 12 12:41:05 2017 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4        }
     1.5      }
     1.6  
     1.7 -    def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
     1.8 +    def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue =
     1.9      {
    1.10        val graph = sessions.build_graph
    1.11        val names = graph.keys
    1.12 @@ -178,7 +178,7 @@
    1.13    private class Job(progress: Progress,
    1.14      name: String,
    1.15      val info: Sessions.Info,
    1.16 -    sessions: Sessions.T,
    1.17 +    sessions: Sessions.Structure,
    1.18      deps: Sessions.Deps,
    1.19      store: Sessions.Store,
    1.20      do_output: Boolean,