39 lines
1.2 KiB
Diff
39 lines
1.2 KiB
Diff
From 6579cf5f72d5de345ae1cc97d0344dfa1771460a Mon Sep 17 00:00:00 2001
|
|
From: "Richard W.M. Jones" <rjones@redhat.com>
|
|
Date: Mon, 28 Jan 2019 22:20:33 +0000
|
|
Subject: [PATCH] Use external command mv to rename old output directory
|
|
(RHBZ#1670191).
|
|
|
|
See https://bugzilla.redhat.com/show_bug.cgi?id=1670191#c0
|
|
for explanation.
|
|
|
|
Thanks: Sam Eiderman
|
|
---
|
|
src/supermin.ml | 10 ++++------
|
|
1 file changed, 4 insertions(+), 6 deletions(-)
|
|
|
|
diff --git a/src/supermin.ml b/src/supermin.ml
|
|
index 71d8b64..7c7135b3 100644
|
|
--- a/src/supermin.ml
|
|
+++ b/src/supermin.ml
|
|
@@ -264,12 +264,10 @@ appliance automatically.
|
|
|
|
(* Delete the old output directory if it exists. *)
|
|
let old_outputdir =
|
|
- try
|
|
- let old_outputdir = outputdir ^ "." ^ string_random8 () in
|
|
- rename outputdir old_outputdir;
|
|
- Some old_outputdir
|
|
- with
|
|
- Unix_error _ -> None in
|
|
+ let old_outputdir = outputdir ^ "." ^ string_random8 () in
|
|
+ let cmd = sprintf "mv %s %s 2>/dev/null"
|
|
+ (quote outputdir) (quote old_outputdir) in
|
|
+ if Sys.command cmd == 0 then Some old_outputdir else None in
|
|
|
|
if debug >= 1 then
|
|
printf "supermin: renaming %s to %s\n%!" new_outputdir outputdir;
|
|
--
|
|
2.22.0
|
|
|