--- a/src/Pure/Tools/server_commands.scala Sat Dec 29 14:58:51 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Sat Dec 29 16:11:24 2018 +0100
@@ -113,15 +113,9 @@
try { Session_Build.command(args.build, progress = progress)._3 }
catch { case exn: Server.Error => error(exn.message) }
- val session =
- Headless.start_session(
- base_info.options,
- base_info.session,
- session_dirs = base_info.dirs,
- session_base = Some(base_info.check_base),
- print_mode = args.print_mode,
- progress = progress,
- log = log)
+ val resources = Headless.Resources(base_info, log = log)
+
+ val session = resources.start_session(print_mode = args.print_mode, progress = progress)
val id = UUID.random()