src/Pure/Tools/server_commands.scala
changeset 67861 cd1cac824ef8
parent 67858 cba5c5657378
child 67862 20a0e0ea6237
--- 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(_))