src/Pure/Tools/build.scala
changeset 62714 63888e5f668b
parent 62704 478b49f0d726
child 62825 e6e80a8bf624
equal deleted inserted replaced
62713:c18a68a3a1f1 62714:63888e5f668b
   445     exclude_sessions: List[String] = Nil,
   445     exclude_sessions: List[String] = Nil,
   446     sessions: List[String] = Nil): Results =
   446     sessions: List[String] = Nil): Results =
   447   {
   447   {
   448     /* session tree and dependencies */
   448     /* session tree and dependencies */
   449 
   449 
   450     val full_tree = Sessions.load(options.int("completion_limit") = 0, dirs, select_dirs)
   450     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
       
   451     val full_tree = Sessions.load(build_options, dirs, select_dirs)
   451     val (selected, selected_tree) =
   452     val (selected, selected_tree) =
   452       full_tree.selection(requirements, all_sessions,
   453       full_tree.selection(requirements, all_sessions,
   453         exclude_session_groups, exclude_sessions, session_groups, sessions)
   454         exclude_session_groups, exclude_sessions, session_groups, sessions)
   454 
   455 
   455     val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
   456     val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)