Skip to content

Commit

Permalink
configure: accept --with-gaproot
Browse files Browse the repository at this point in the history
  • Loading branch information
fingolfin committed Jan 3, 2023
1 parent a577f43 commit 5dfecc6
Showing 1 changed file with 31 additions and 12 deletions.
43 changes: 31 additions & 12 deletions configure
Original file line number Diff line number Diff line change
@@ -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."

0 comments on commit 5dfecc6

Please sign in to comment.