# HG changeset patch
# User wenzelm
# Date 949092923 -3600
# Node ID 0b5be7287661386dc698ea2168aef99c78d4fc0c
# Parent  020e384e67dd01a7eddb1b108e4f7a41b11daef5
cp -r;

diff -r 020e384e67dd -r 0b5be7287661 src/Pure/General/file.ML
--- 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 *)