# HG changeset patch
# User wenzelm
# Date 1520972522 -3600
# Node ID 74e2a4b62826846de5b205815a638dceb9d5b65d
# Parent  f701a1d5d8528166d4d557b00cf691b7fe8598bb
more options;

diff -r f701a1d5d852 -r 74e2a4b62826 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Tue Mar 13 21:04:42 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Tue Mar 13 21:22:02 2018 +0100
@@ -20,7 +20,8 @@
       all_known: Boolean = false,
       focus_session: Boolean = false,
       required_session: Boolean = false,
-      system_mode: Boolean = false)
+      system_mode: Boolean = false,
+      verbose: Boolean = false)
 
     def unapply(json: JSON.T): Option[Args] =
       for {
@@ -33,11 +34,12 @@
         focus_session <- JSON.bool_default(json, "focus_session")
         required_session <- JSON.bool_default(json, "required_session")
         system_mode <- JSON.bool_default(json, "system_mode")
+        verbose <- JSON.bool_default(json, "verbose")
       }
       yield {
         Args(session, prefs = prefs, opts = opts, dirs = dirs, ancestor_session = ancestor_session,
           all_known = all_known, focus_session = focus_session, required_session = required_session,
-          system_mode = system_mode)
+          system_mode = system_mode, verbose = verbose)
       }
 
     def command(progress: Progress, args: Args): (JSON.T, Sessions.Base_Info, Build.Results) =
@@ -63,6 +65,7 @@
           system_mode = args.system_mode,
           dirs = dirs,
           infos = base_info.infos,
+          verbose = args.verbose,
           sessions = List(args.session))
 
       (JSON.Object("rc" -> results.rc), base_info, results)