proper build command;
authorFabian Huch <huch@in.tum.de>
Fri, 28 Jun 2024 13:49:29 +0200
changeset 80422 23569f8a62e9
parent 80421 96e1b4f38a17
child 80423 797196669573
proper build command;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jun 28 12:10:26 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Fri Jun 28 13:49:29 2024 +0200
@@ -88,13 +88,16 @@
         build_hosts.map(host => " -H " + Bash.string(host.print)).mkString +
         if_proper(presentation, " -P:") +
         if_proper(requirements, " -R") +
+        exclude_session_groups.map(session => " -X " + Bash.string(session)).mkString +
         if_proper(all_sessions, " -a") +
         if_proper(build_heap, " -b") +
         if_proper(clean_build, " -c") +
         if_proper(export_files, " -e") +
         if_proper(fresh_build, " -f") +
+        session_groups.map(session => " -g " + Bash.string(session)).mkString +
         Options.Spec.bash_strings(prefs, bg = true) +
         if_proper(verbose, " -v") +
+        exclude_sessions.map(session => " -x " + Bash.string(session)).mkString +
         sessions.map(session => " " + Bash.string(session)).mkString
     }
   }