diff -r 72f6d6fd5853 -r 30e9ff9be90a src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sat Feb 13 17:27:23 2016 +0100
+++ b/src/Pure/General/file.scala	Sat Feb 13 19:52:56 2016 +0100
@@ -102,8 +102,9 @@
 
   /* shell path (bash) */
 
-  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
-  def shell_path(file: JFile): String = "'" + standard_path(file) + "'"
+  def shell_quote(s: String): String = "'" + s + "'"
+  def shell_path(path: Path): String = shell_quote(standard_path(path))
+  def shell_path(file: JFile): String = shell_quote(standard_path(file))
 
 
   /* directory content */