moved copy_all to Thy/present.ML;
authorwenzelm
Fri, 15 Feb 2002 20:42:00 +0100
changeset 12894 61f485eb0dc2
parent 12893 cbb4dc5e6478
child 12895 d9dd528ecea6
moved copy_all to Thy/present.ML;
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 *)