diff -r 269dc4bf1f40 -r 23d0a45a9283 src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala Fri Mar 27 12:46:56 2020 +0100 +++ b/src/Pure/Tools/server_commands.scala Fri Mar 27 13:02:56 2020 +0100 @@ -46,7 +46,7 @@ } def command(args: Args, progress: Progress = No_Progress) - : (JSON.Object.T, Build.Results, Sessions.Base_Info) = + : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = { val options = Options.init(prefs = args.preferences, opts = args.options) val dirs = args.dirs.map(Path.explode(_)) @@ -85,7 +85,7 @@ "timing" -> result.timing.json) })) - if (results.ok) (results_json, results, base_info) + if (results.ok) (results_json, results, options, base_info) else throw new Server.Error("Session build failed: return code " + results.rc, results_json) } } @@ -106,11 +106,11 @@ def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger) : (JSON.Object.T, (UUID.T, Headless.Session)) = { - val base_info = - try { Session_Build.command(args.build, progress = progress)._3 } + val (_, _, options, base_info) = + try { Session_Build.command(args.build, progress = progress) } catch { case exn: Server.Error => error(exn.message) } - val resources = Headless.Resources(base_info, log = log) + val resources = Headless.Resources(options, base_info, log = log) val session = resources.start_session(print_mode = args.print_mode, progress = progress)