[PATCH] Chop final '/' in output directory (RHBZ#1146753)

[Pino Toscano]

If the specified output directory ends with a slash, chop it then;
leaving it in will create problems later, like creating the temporary
directory inside the output directory (and not aside it), and trying to
rename it to the directory containing it (which will fail indeed).
---
 src/supermin.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/supermin.ml b/src/supermin.ml
index 9623229..3070b6b 100644
--- a/src/supermin.ml
+++ b/src/supermin.ml
@@ -186,6 +186,11 @@ let main () =
       eprintf "supermin: output directory (-o option) must be supplied\n";
       exit 1
     );
+    (* Chop final '/' in output directory (RHBZ#1146753). *)
+    let outputdir =
+      let len = String.length outputdir in
+      if outputdir.[len - 1] == '/' then String.sub outputdir 0 (len - 1)
+      else outputdir in
 
     debug, mode, if_newer, inputs, lockfile, outputdir,
     (copy_kernel, dtb_wildcard, format, host_cpu,
-- 
2.1.0