src/Pure/Tools/build.scala
changeset 66968 9991671c98aa
parent 66962 e1bde71bace6
child 66972 f65fc869e835
     1.1 --- a/src/Pure/Tools/build.scala	Tue Oct 31 20:57:44 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Oct 31 21:50:09 2017 +0100
     1.3 @@ -354,6 +354,7 @@
     1.4      clean_build: Boolean = false,
     1.5      dirs: List[Path] = Nil,
     1.6      select_dirs: List[Path] = Nil,
     1.7 +    infos: List[Sessions.Info] = Nil,
     1.8      numa_shuffling: Boolean = false,
     1.9      max_jobs: Int = 1,
    1.10      list_files: Boolean = false,
    1.11 @@ -381,7 +382,7 @@
    1.12      /* session selection and dependencies */
    1.13  
    1.14      val full_sessions =
    1.15 -      Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs)
    1.16 +      Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
    1.17  
    1.18      def sources_stamp(deps: Sessions.Deps, name: String): String =
    1.19      {