add rebuild-dune.sh

parent f936343b
#!/bin/bash
set -e
if [ "X${OPTS}" == "X" ]; then
echo You have to define OPTS, i.e. export OPTS=gcc-relwithdebinfo
exit
fi
# define environment in case we are not in one of our dockers
# determines which one to use below environments/
if [ "X${DXT_ENVIRONMENT}" == "X" ]; then
export DXT_ENVIRONMENT=debian-full
fi
# check existence of the virtualenv
if [ "X$e/${DXT_ENVIRONMENT}/venv/dune-${OPTS}" == "X" ]; then
echo Missing virtualenv, did you call setup.sh?
exit
fi
# load the variables of this environment, sources the virtualenv
source e/${DXT_ENVIRONMENT}/PATH.sh
# build dune
NPROC=$(($(nproc) - 1))
./dune-common/bin/dunecontrol --opts=config.opts/$OPTS --builddir=$INSTALL_PREFIX/build-$OPTS configure
./dune-common/bin/dunecontrol --opts=config.opts/$OPTS --builddir=$INSTALL_PREFIX/build-$OPTS bexec 'make -j$NPROC all'
./dune-common/bin/dunecontrol --opts=config.opts/$OPTS --builddir=$INSTALL_PREFIX/build-$OPTS bexec 'make -j$NPROC bindings || echo no bindings'
./dune-common/bin/dunecontrol --opts=config.opts/$OPTS --builddir=$INSTALL_PREFIX/build-$OPTS bexec 'make install_python'
echo
echo "All done! From now on run"
echo " export OPTS=$OPTS"
echo " source e/${DXT_ENVIRONMENT}/PATH.sh"
echo "to activate the virtualenv!"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment