# HG changeset patch
# User wenzelm
# Date 967823107 -7200
# Node ID 1634fdb11b001881a410d0e0e5b04a1481d81a97
# Parent  d8f8dc335c8c44f63d5f828b6176f5ba5ff84995
isatool_document: quote args;

diff -r d8f8dc335c8c -r 1634fdb11b00 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Sep 01 17:44:44 2000 +0200
+++ b/src/Pure/Thy/present.ML	Fri Sep 01 17:45:07 2000 +0200
@@ -253,7 +253,7 @@
 fun copy_files path1 path2 =
   (File.mkdir path2;
    File.system_command
-     ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
+     ("cp " ^ File.quote_sysify_path path1 ^ " " ^ File.quote_sysify_path path2));
 
 
 fun init false _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
@@ -311,7 +311,8 @@
 
 fun isatool_document doc_format doc_prefix =
   let
-    val cmd = "$ISATOOL document -c -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'";
+    val cmd =
+      "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^ File.quote_sysify_path doc_prefix;
   in
     writeln cmd;
     if system cmd <> 0 orelse not (File.exists (Path.ext doc_format doc_prefix)) then