diff -r 5a6c483269f3 -r cd1cac824ef8 src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala Wed Mar 14 20:20:10 2018 +0100 +++ b/src/Pure/Tools/server_commands.scala Wed Mar 14 20:29:46 2018 +0100 @@ -42,7 +42,8 @@ system_mode = system_mode, verbose = verbose) } - def command(progress: Progress, args: Args): (JSON.T, Build.Results, Sessions.Base_Info) = + def command(progress: Progress, args: Args) + : (JSON.Object.T, Build.Results, Sessions.Base_Info) = { val options = Options.init(prefs = args.prefs, opts = args.opts) val dirs = args.dirs.map(Path.explode(_))