From 5dfecc6b4d48436ec3265c67b12701e4c48eae93 Mon Sep 17 00:00:00 2001 From: Max Horn Date: Tue, 3 Jan 2023 17:46:07 +0100 Subject: [PATCH] configure: accept --with-gaproot --- configure | 43 +++++++++++++++++++++++++++++++------------ 1 file changed, 31 insertions(+), 12 deletions(-) diff --git a/configure b/configure index 9bfc538..dbf5b78 100755 --- a/configure +++ b/configure @@ -1,17 +1,36 @@ #!/bin/sh # usage: configure gappath -# this script creates a `Makefile' from `Makefile.in' -if test -z $1; then - GAPPATH=../..; echo "Using ../.. as default GAP path"; -else - GAPPATH=$1; -fi -if ! test -e $GAPPATH/sysinfo.gap; then - echo "Please give correct GAP path as argument (and make sure that GAP" - echo "is already properly installed)." - exit +# this script creates a `Makefile' from `Makefile.in' + +set -e + +GAPPATH=../.. +while test "$#" -ge 1 ; do + option="$1" ; shift + case "$option" in + --with-gaproot=*) GAPPATH=${option#--with-gaproot=}; ;; + -*) echo "ERROR: unsupported argument $option" ; exit 1;; + *) GAPPATH="$option" ;; + esac +done + +if test ! -r "$GAPPATH/sysinfo.gap" ; then + echo + echo "No file $GAPPATH/sysinfo.gap found." + echo + echo "Usage: ./configure [GAPPATH]" + echo " where GAPPATH is a path to your GAP installation" + echo " (The default for GAPPATH is \"../..\")" + echo + echo "Either your GAPPATH is incorrect or the GAP it is pointing to" + echo "is not properly compiled (do \"./configure && make\" there first)." + echo + echo "Aborting... No Makefile is generated." + echo + exit 1 fi -. $GAPPATH/sysinfo.gap +echo "Using settings from $GAPPATH/sysinfo.gap" +rm -f Makefile +. "$GAPPATH/sysinfo.gap" sed -e "s|@GAPARCH@|$GAParch|g" Makefile.in > Makefile -echo "Makefile successfully created."