# HG changeset patch
# User kleing
# Date 1013891179 -3600
# Node ID c78872ea33209275f3ea182ffbd321db2ac1c2b5
# Parent  f4d10ad0ea7bf6d9a75c6859ef285248d5c25eed
fixed copy_all

diff -r f4d10ad0ea7b -r c78872ea3320 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Feb 16 20:59:34 2002 +0100
+++ b/src/Pure/Thy/present.ML	Sat Feb 16 21:26:19 2002 +0100
@@ -269,9 +269,9 @@
   system ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2));  (*FIXME: quote!?*)
 
 fun copy_all path1 path2 =
- (File.mkdir path2;
-  system ("cp -r " ^ File.quote_sysify_path path1 ^ " " ^
-    File.quote_sysify_path (Path.append path2 Path.parent)));
+ (File.mkdir path2;  
+  system ("cp -r " ^ File.quote_sysify_path path1 ^ "/. " ^
+    File.quote_sysify_path path2));
 
 
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);