diff --git a/tools/ci-build b/tools/ci-build index 89c4cb8d3..52d22ee80 100755 --- a/tools/ci-build +++ b/tools/ci-build @@ -131,6 +131,9 @@ case "${OCAML_ARCH}" in *) arch_error;; esac +# Make sure two builds won't use the same install directory +instdir="$instdir-$$" + ######################################################################### # On Windows, cleanup processes that may remain from previous run