# HG changeset patch
# User wenzelm
# Date 967830544 -7200
# Node ID c362e75e89395b882226a414d1a8e384c07b507a
# Parent  2be239143d422e16141a2fb006ab9cccbe26b6da
copy_files: do not quote paths (for now);

diff -r 2be239143d42 -r c362e75e8939 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Sep 01 19:42:11 2000 +0200
+++ b/src/Pure/Thy/present.ML	Fri Sep 01 19:49:04 2000 +0200
@@ -252,8 +252,8 @@
 
 fun copy_files path1 path2 =
   (File.mkdir path2;
-   File.system_command
-     ("cp " ^ File.quote_sysify_path path1 ^ " " ^ File.quote_sysify_path path2));
+   File.system_command  (*FIXME: quote paths!?*)
+     ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));
 
 
 fun init false _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)