equal
deleted
inserted
replaced
71 val options = Options.init(prefs = args.preferences, opts = args.options) |
71 val options = Options.init(prefs = args.preferences, opts = args.options) |
72 val dirs = args.dirs.map(Path.explode) |
72 val dirs = args.dirs.map(Path.explode) |
73 |
73 |
74 val base_info = |
74 val base_info = |
75 Sessions.base_info(options, args.session, progress = progress, dirs = dirs, |
75 Sessions.base_info(options, args.session, progress = progress, dirs = dirs, |
76 include_sessions = args.include_sessions) |
76 include_sessions = args.include_sessions).check |
77 val base = base_info.check_base |
|
78 |
77 |
79 val results = |
78 val results = |
80 Build.build(options, |
79 Build.build(options, |
81 selection = Sessions.Selection.session(args.session), |
80 selection = Sessions.Selection.session(args.session), |
82 progress = progress, |
81 progress = progress, |