| changeset 8163 | 0b5be7287661 |
| parent 7850 | 3689adcf9b8b |
| child 8806 | a202293db3f6 |
--- 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 *)