equal
deleted
inserted
replaced
37 case bad => error("No documentation session for " + commas_quote(bad)) |
37 case bad => error("No documentation session for " + commas_quote(bad)) |
38 } |
38 } |
39 |
39 |
40 progress.echo("Build started for sessions " + commas_quote(selection.sessions)) |
40 progress.echo("Build started for sessions " + commas_quote(selection.sessions)) |
41 val build_results = |
41 val build_results = |
42 Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs) |
42 Build.build(options, selection = selection, progress = progress, max_jobs = max_jobs).check |
43 if (!build_results.ok) error("Build failed") |
|
44 |
43 |
45 progress.echo("Build started for documentation " + commas_quote(documents)) |
44 progress.echo("Build started for documentation " + commas_quote(documents)) |
46 val deps = Sessions.load_structure(options + "document").selection_deps(selection) |
45 val deps = Sessions.load_structure(options + "document").selection_deps(selection) |
47 |
46 |
48 val errs = |
47 val errs = |