# HG changeset patch
# User wenzelm
# Date 1495618740 -7200
# Node ID 5b8ed310b31dd6202a9e2fc1e104695f463b8c20
# Parent  49f61e2f5a023d87ab90a1e5937abef6990fe0a4
tuned;

diff -r 49f61e2f5a02 -r 5b8ed310b31d src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Wed May 24 11:17:23 2017 +0200
+++ b/src/Pure/Admin/other_isabelle.scala	Wed May 24 11:39:00 2017 +0200
@@ -15,8 +15,7 @@
   /* static system */
 
   def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
-    progress.bash(
-      "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" + script,
+    progress.bash(Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
       env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo)
 
   def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
diff -r 49f61e2f5a02 -r 5b8ed310b31d src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed May 24 11:17:23 2017 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed May 24 11:39:00 2017 +0200
@@ -335,6 +335,10 @@
   def pdf_viewer(arg: Path): Unit =
     bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
 
+  def export_isabelle_identifier(isabelle_identifier: String): String =
+    if (isabelle_identifier == "") ""
+    else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
+
 
 
   /** Isabelle resources **/