--- a/src/Pure/Tools/server_commands.scala Mon Mar 13 15:35:15 2023 +0100
+++ b/src/Pure/Tools/server_commands.scala Mon Mar 13 15:53:31 2023 +0100
@@ -61,7 +61,8 @@
args: Args,
progress: Progress = new Progress
) : (JSON.Object.T, Build.Results, Options, Sessions.Background) = {
- val options = Options.init(prefs = args.preferences, opts = args.options)
+ val options =
+ Options.init(prefs = args.preferences, specs = args.options.map(Options.Spec.make))
val dirs = args.dirs.map(Path.explode)
val session_background =