# HG changeset patch
# User wenzelm
# Date 1744230239 -7200
# Node ID d5ef492dd6739c3de8058344882ab2be667d39b6
# Parent  3cc075052033d23993f5f8973355987270434a2c
tuned: prefer explicit Bash.exports;

diff -r 3cc075052033 -r d5ef492dd673 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Wed Apr 09 17:40:27 2025 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Apr 09 22:23:59 2025 +0200
@@ -664,7 +664,7 @@
         val log_opts = "--graph --color always"
         val rev1 = "children(" + rev0 + ")"
         val cmd = repository.command_line("log", Mercurial.opt_rev(rev1 + ":" + rev), log_opts)
-        val log = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
+        val log = Isabelle_System.bash(Bash.exports("HGPLAINEXCEPT=color") + cmd).check.out
         if (log.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(log_ext).gz, log)
       }
 
@@ -677,7 +677,7 @@
       if (rev0.nonEmpty && rev.nonEmpty) {
         val diff_opts = "--noprefix --nodates --ignore-all-space --color always"
         val cmd = repository.command_line("diff", Mercurial.opt_rev(rev0 + ":" + rev), diff_opts)
-        val diff = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out
+        val diff = Isabelle_System.bash(Bash.exports("HGPLAINEXCEPT=color") + cmd).check.out
         if (diff.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(diff_ext).gz, diff)
       }
 
diff -r 3cc075052033 -r d5ef492dd673 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Wed Apr 09 17:40:27 2025 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Apr 09 22:23:59 2025 +0200
@@ -223,7 +223,8 @@
       options: String = "",
       repository: Boolean = true
     ): String = {
-      "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
+      Bash.exports("LANG=C", "HGPLAIN=") +
+        "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
         (if (repository) " --repository " + ssh.bash_path(root) else "") +
         " --noninteractive " + name + " " + options + " " + args
     }
diff -r 3cc075052033 -r d5ef492dd673 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Apr 09 17:40:27 2025 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed Apr 09 22:23:59 2025 +0200
@@ -57,8 +57,7 @@
       if (props.nonEmpty) consume(props)
     }
 
-    val env_prefix =
-      if_proper(stats_dir, "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n")
+    val env_prefix = if_proper(stats_dir, Bash.exports("POLYSTATSDIR=" + stats_dir))
 
     Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
         Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
diff -r 3cc075052033 -r d5ef492dd673 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Wed Apr 09 17:40:27 2025 +0200
+++ b/src/Pure/System/bash.scala	Wed Apr 09 22:23:59 2025 +0200
@@ -53,10 +53,8 @@
     isabelle_identifier: String = "",
     cwd: Path = Path.current
   ): String = {
-    if_proper(user_home,
-      "export USER_HOME=" + Bash.string(user_home) + "\n") +
-    if_proper(isabelle_identifier,
-      "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n") +
+    if_proper(user_home, exports("USER_HOME=" + user_home)) +
+    if_proper(isabelle_identifier, exports("ISABELLE_IDENTIFIER=" + isabelle_identifier)) +
     (if (cwd == null || cwd.is_current) "" else "cd " + quote(cwd.implode) + "\n") +
     script
   }