src/Pure/General/file.ML
changeset 12894 61f485eb0dc2
parent 12116 4027b15377a5
child 14981 e73f8140af78
--- 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 *)