tools/ci-build: install to a different directory for each build
This commit ensures the install directory will be distinct for each build, with the two following motivations: 1. If required, it will make it possible to have several builds running concurrently on the same slave without conflicts between their make install 2. So far, if for any reason make install fails, then the build script gets stopped and the install directory will not be removed. Thus if a future build tries to install to the same directory, its installation could in principle fail, not because it is broken but because the previous build has left the install directory in a corrupted state. So this commit ensures that make install will be done in an empty directory.master
parent
023f3e3fa2
commit
67276a09af
|
@ -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
|
||||
|
||||
|
|
Loading…
Reference in New Issue