equal
deleted
inserted
replaced
72 Build.build(options, |
72 Build.build(options, |
73 selection = Sessions.Selection.session(args.session), |
73 selection = Sessions.Selection.session(args.session), |
74 progress = progress, |
74 progress = progress, |
75 build_heap = true, |
75 build_heap = true, |
76 dirs = dirs, |
76 dirs = dirs, |
77 infos = session_background.infos, |
77 infos = session_background.infos) |
78 verbose = progress.verbose) |
|
79 |
78 |
80 val sessions_order = |
79 val sessions_order = |
81 session_background.sessions_structure.imports_topological_order.zipWithIndex. |
80 session_background.sessions_structure.imports_topological_order.zipWithIndex. |
82 toMap.withDefaultValue(-1) |
81 toMap.withDefaultValue(-1) |
83 |
82 |