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)