diff -r 70e288a4b32d -r cb212f52c2a3 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 =