-function push_PREFIX_ARG ()
-{
- if [[ -n "$OLD_PREFIX_ARG" ]]; then
- die "OLD_PREFIX_ARG was set on push, programmer error!"
- fi
-
- if [[ -n "$PREFIX_ARG" ]]; then
- OLD_PREFIX_ARG=$PREFIX_ARG
- PREFIX_ARG=
- fi
-
- if [[ -n "$1" ]]; then
- PREFIX_ARG="--prefix=$1"
- fi
-}
-
-function pop_PREFIX_ARG ()
-{
- if [[ -n "$OLD_PREFIX_ARG" ]]; then
- PREFIX_ARG=$OLD_PREFIX_ARG
- OLD_PREFIX_ARG=
- else
- PREFIX_ARG=
- fi
-}
-
-function push_TESTS_ENVIRONMENT ()
-{
- if [[ -n "$OLD_TESTS_ENVIRONMENT" ]]; then
- die "OLD_TESTS_ENVIRONMENT was set on push, programmer error!"
- fi
-
- if [[ -n "$TESTS_ENVIRONMENT" ]]; then
- OLD_TESTS_ENVIRONMENT=$TESTS_ENVIRONMENT
- TESTS_ENVIRONMENT=
- fi
-}
-
-function pop_TESTS_ENVIRONMENT ()
-{
- TESTS_ENVIRONMENT=
- if [[ -n "$OLD_TESTS_ENVIRONMENT" ]]; then
- TESTS_ENVIRONMENT=$OLD_TESTS_ENVIRONMENT
- OLD_TESTS_ENVIRONMENT=
- fi
-}
-
-function safe_pushd ()
-{
- pushd $1 &> /dev/null ;
-
- if [ -n "$BUILD_DIR" ]; then
- if $VERBOSE; then
- echo "BUILD_DIR=$BUILD_DIR"
- fi
- fi
-}
-
-function safe_popd ()
-{
- local directory_to_delete=`pwd`
- popd &> /dev/null ;
- if [ $? -eq 0 ]; then
- if [[ "$top_srcdir" == "$directory_to_delete" ]]; then
- die "We almost deleted top_srcdir($top_srcdir), programmer error"
- fi
-
- rm -r -f "$directory_to_delete"
- fi
-}
-
-function make_valgrind ()