# HG changeset patch
# User wenzelm
# Date 1118077114 -7200
# Node ID 5e845b75f94f9e0e32165f2b254fa1359144502a
# Parent  fee0a02f61bb22cbcd65cdb1da097562da980228
copy_dir: be permissive wrt. errors;

diff -r fee0a02f61bb -r 5e845b75f94f src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Jun 06 15:09:47 2005 +0200
+++ b/src/Pure/General/file.ML	Mon Jun 06 18:58:34 2005 +0200
@@ -126,7 +126,7 @@
   in write target (read from) end;
 
 fun copy_dir from to =
-  system_command ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to);
+  (system ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to); ());  (* FIXME system_command *)
 
 
 (* use ML files *)