# HG changeset patch
# User wenzelm
# Date 1459795554 -7200
# Node ID d8cf59edf819bcadb54b0df191871bcb1ff4822d
# Parent  8e54fd480809dd17443efeb9c528045cde2e33d9
allow empty string;

diff -r 8e54fd480809 -r d8cf59edf819 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Apr 04 20:28:17 2016 +0200
+++ b/src/Pure/General/file.ML	Mon Apr 04 20:45:54 2016 +0200
@@ -46,21 +46,22 @@
 val standard_path = Path.implode o Path.expand;
 val platform_path = ML_System.platform_path o standard_path;
 
-val bash_string =
-  translate_string (fn ch =>
-    let val c = ord ch in
-      (case ch of
-        "\t" => "$'\\t'"
-      | "\n" => "$'\\n'"
-      | "\f" => "$'\\f'"
-      | "\r" => "$'\\r'"
-      | _ =>
-          if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
-            exists_string (fn c => c = ch) "-./:_" then ch
-          else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
-          else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
-          else "\\" ^ ch)
-    end);
+fun bash_string "" = "\"\""
+  | bash_string str =
+      str |> translate_string (fn ch =>
+        let val c = ord ch in
+          (case ch of
+            "\t" => "$'\\t'"
+          | "\n" => "$'\\n'"
+          | "\f" => "$'\\f'"
+          | "\r" => "$'\\r'"
+          | _ =>
+              if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
+                exists_string (fn c => c = ch) "-./:_" then ch
+              else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
+              else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
+              else "\\" ^ ch)
+        end);
 
 val bash_args = space_implode " " o map bash_string;
 
diff -r 8e54fd480809 -r d8cf59edf819 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Apr 04 20:28:17 2016 +0200
+++ b/src/Pure/General/file.scala	Mon Apr 04 20:45:54 2016 +0200
@@ -123,7 +123,8 @@
   }
 
   def bash_string(s: String): String =
-    UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
+    if (s == "") "\"\""
+    else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
 
   def bash_args(args: List[String]): String =
     args.iterator.map(bash_string(_)).mkString(" ")