--- 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(_))