|
|
|
|
Quelle configure
Sprache: unbekannt
|
|
|
#!/bin/sh
# usage: configure gappath
# 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
echo "Using settings from $GAPPATH/sysinfo.gap"
rm -f Makefile
. "$GAPPATH/sysinfo.gap"
sed -e "s|@GAPARCH@|$GAParch|g" Makefile.in > Makefile
[ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
]
|
2026-03-28
|
|
|
|
|
