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

[Pádraig Brady]

On 15/10/15 14:39, Pino Toscano wrote:
> 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,
> 

Wrong list. Ignoring...