# HG changeset patch
# User wenzelm
# Date 1457876527 -3600
# Node ID b89d4b320464d665fe105b9fcc7b6f887c026ae1
# Parent  8e5b631d203b683f4dbe3163912e8b399807ed1e
tuned;

diff -r 8e5b631d203b -r b89d4b320464 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Mar 13 14:27:31 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Mar 13 14:42:07 2016 +0100
@@ -307,10 +307,10 @@
   }
 
   def open(arg: String): Unit =
-    bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
+    bash("exec \"$ISABELLE_OPEN\" " + File.bash_string(arg) + " >/dev/null 2>/dev/null &")
 
   def pdf_viewer(arg: Path): Unit =
-    bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
+    bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
 
   def hg(cmd_line: String, cwd: JFile = null): Process_Result =
     bash("\"${HG:-hg}\" " + cmd_line, cwd = cwd)