#!/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"
sed -e "s;@GAPPATH@;$GAPPATH;g" Makefile.in > Makefile
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
