#!/bin/sh #--------------------------------------------------------------------------# # Run './configure' to produce a 'makefile' in the 'build' sub-directory or # in any immediate sub-directory different from the 'src', 'scripts' and # 'test' directories. #--------------------------------------------------------------------------# rm -f configure.log #--------------------------------------------------------------------------# # Common default options. all=no debug=no libs="" logging=no check=no competition=no coverage=no flexible=yes profile=no contracts=yes tracing=yes unlocked=yes pedantic=no options="" quiet=no m32=no contrib=yes ipasir=yes #--------------------------------------------------------------------------# if [ -f ./scripts/colors.sh ] then . ./scripts/colors.sh elif [ -f ../scripts/colors.sh ] then . ../scripts/colors.sh else BAD="" HILITE="" BOLD="" NORMAL="" fi die () { if [ -f configure.log ] then checklog=" (check also 'configure.log')" else checklog="" fi cecho "${BOLD}configure:${NORMAL} ${BAD}error:${NORMAL} $*${checklog}" exit 1 } rm -f configure.log msg () { cecho "${BOLD}configure:${NORMAL} $*" } # if we can find the 'color.sh' script source it and overwrite color codes for dir in . .. do [ -f $dir/scripts/colors.sh ] || continue . $dir/scripts/colors.sh || exit 1 break done #--------------------------------------------------------------------------# # Parse and handle command line options. usage () { cat << EOF usage: configure [