diff --git a/headers/hdrck.ml b/headers/hdrck.ml index 96232626de0c1bfeeeed09e770f345193fa02c73..692c80226819e5a076d40b4f454249e4134b7ee1 100755 --- a/headers/hdrck.ml +++ b/headers/hdrck.ml @@ -135,7 +135,11 @@ let error ~exit_value = in the header_spec.txt files. *) let path_concat p1 p2 = - p1 ^ "/" ^ p2 + (* Note: use String.ends_with when minimum OCaml version is 4.13 *) + if String.length p1 > 0 && String.get p1 (String.length p1 - 1) = '/' then + p1 ^ p2 + else + p1 ^ "/" ^ p2 (* Temporary directory management (cont.) *) let get_tmp_dirname () = match !tmp_dirname with