clarified copy_file: allow to rename base name, e.g. relevant for 'display_drafts';
authorwenzelm
Sat, 24 May 2014 21:27:15 +0200
changeset 57085 cb212f52c2a3
parent 57084 70e288a4b32d
child 57086 db7c735e963d
clarified copy_file: allow to rename base name, e.g. relevant for 'display_drafts';
src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sat May 24 20:24:43 2014 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sat May 24 21:27:15 2014 +0200
@@ -72,14 +72,11 @@
   let
     val src = Path.expand src0;
     val dst = Path.expand dst0;
-    val (target_dir, target) =
-      if File.is_dir dst then (dst, Path.append dst (Path.base src))
-      else (Path.dir dst, dst);
+    val target = if File.is_dir dst then Path.append dst (Path.base src) else dst;
   in
     if File.eq (src, target) then ()
     else
-      (ignore o system_command)
-        ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target_dir ^ "/.")
+      ignore (system_command ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target))
   end;
 
 fun copy_file_base (base_dir, src0) target_dir =