Allow to pass custom location for the Boost library for Spike (#2082)

This commit is contained in:
Cesar Fuguet 2024-04-29 12:04:20 +02:00 committed by GitHub
parent 3919e79f8f
commit 0c2108845a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -41,8 +41,12 @@ if ! [ -f "$SPIKE_INSTALL_DIR/bin/spike" ]; then
# Build and install Spike (including extensions).
mkdir -p build
cd build
WITH_BOOST=""
if [[ ! -z "$BOOST_INSTALL_DIR" ]]; then
WITH_BOOST="--with-boost=${BOOST_INSTALL_DIR}"
fi
if [[ ! -f config.log ]]; then
../configure --prefix="$SPIKE_INSTALL_DIR"
../configure --prefix="$SPIKE_INSTALL_DIR" ${WITH_BOOST}
fi
make -j${NUM_JOBS}
echo "Installing Spike in '$SPIKE_INSTALL_DIR'..."