--- a/src/Pure/General/file.ML Sat Dec 30 12:41:59 2006 +0100
+++ b/src/Pure/General/file.ML Sat Dec 30 16:08:00 2006 +0100
@@ -137,12 +137,15 @@
SOME ids => OS.FileSys.compare ids = EQUAL
| NONE => false);
-fun copy src dst = conditional (not (eq (src, dst))) (fn () =>
- let val target = if is_dir dst then Path.append dst (Path.base src) else dst
- in write target (read src) end);
+fun copy src dst =
+ if eq (src, dst) then ()
+ else
+ let val target = if is_dir dst then Path.append dst (Path.base src) else dst
+ in write target (read src) end;
-fun copy_dir src dst = conditional (not (eq (src, dst))) (fn () =>
- (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ()))
+fun copy_dir src dst =
+ if eq (src, dst) then ()
+ else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
(* use ML files *)