# HG changeset patch
# User wenzelm
# Date 1013802120 -3600
# Node ID 61f485eb0dc2521608e72e414364966c1fe83a9d
# Parent  cbb4dc5e64788db0978ed78722190aeeaf87d9c4
moved copy_all to Thy/present.ML;

diff -r cbb4dc5e6478 -r 61f485eb0dc2 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Fri Feb 15 20:41:39 2002 +0100
+++ b/src/Pure/General/file.ML	Fri Feb 15 20:42:00 2002 +0100
@@ -26,7 +26,6 @@
   val info: Path.T -> info option
   val exists: Path.T -> bool
   val mkdir: Path.T -> unit
-  val copy_all: Path.T -> Path.T -> unit
   val use: Path.T -> unit
 end;
 
@@ -98,12 +97,9 @@
 fun system_command cmd =
   if system cmd <> 0 then error ("System command failed: " ^ cmd)
   else ();
-    
+
 fun mkdir path = system_command ("mkdir -p " ^ quote_sysify_path path);
 
-fun copy_all path1 path2 =  (*dereferences symlinks!*)
-  system_command ("cp -r " ^ quote_sysify_path path1 ^ " " ^ quote_sysify_path path2);
-
 
 (* use ML files *)