cp -r;

--- a/src/Pure/General/file.ML	Fri Jan 28 15:26:51 2000 +0100
+++ b/src/Pure/General/file.ML	Fri Jan 28 21:55:23 2000 +0100
@@ -100,8 +100,8 @@
     
 fun mkdir path = system_command ("mkdir -p " ^ quote_sysify path);
 
-fun copy_all path1 path2 =
-  system_command ("cp -R " ^ quote_sysify path1 ^ " " ^ quote_sysify path2);
+fun copy_all path1 path2 =  (*dereferences symlinks!*)
+  system_command ("cp -r " ^ quote_sysify path1 ^ " " ^ quote_sysify path2);
 
 
 (* symbol_use *)