https://github.com/frankluebeck/EDIM
Raw File
Tip revision: 064e52cef5d5ec7840348c47b47914f4852a1d87 authored by Frank Lübeck on 29 January 2018, 23:14:40 UTC
Initialize with files from 1.3.2 release
Tip revision: 064e52c
configure
#!/bin/sh
# (C) Frank Lübeck 2011
# configure script for Browse, EDIM and other packages
# usage: ./configure [GAPPATH] [CONFIGNAME=myconf]
# this script creates a "Makefile-myconf" from "Makefile.in" with
# a link to "Makefile"

# some tools on OS X made locale related problems, so:
export LANG=C
export LC_ALL=C

# read arguments
while [ x"$1" != "x" ]; do
  if [ ${1#CONFIGNAME=} = ${1} ]; then
    GAPPATH=$1
  else
    eval $1
  fi
  shift
done

if [ x"$GAPPATH" = "x" ]; then 
    GAPPATH=../..
    echo "Using ../.. as default GAPPATH" 
fi

if [ x"$CONFIGNAME" = "x" ]; then
  CONFIGNAME="default64"
  if [ ! -e $GAPPATH/sysinfo.gap-$CONFIGNAME ]; then
    CONFIGNAME="default32"
  fi 
fi

if [ ! -e $GAPPATH/sysinfo.gap-$CONFIGNAME ]; then
    echo
    echo "No file "$GAPPATH"/sysinfo.gap-"$CONFIGNAME" found."
    echo  
    echo "Usage: ./configure [GAPPATH] [CONFIGNAME=confnam]"
    echo "       where GAPPATH is a path to your GAP installation"
    echo "       and confnam is the name of the GAP configuration to use."
    echo "       (The default for GAPPATH is \"../..\" and default confignam"
    echo "       is \"default64\" if it exists, otherwise \"default32\".)"
    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 config in "$GAPPATH"/sysinfo.gap-"$CONFIGNAME

rm -f Makefile Makefile-$CONFIGNAME
. $GAPPATH/sysinfo.gap-$CONFIGNAME
GAParchprot="$GAParch"
echo GAPPATH=$GAPPATH >Makefile-$CONFIGNAME 
echo CONFIGNAME=$CONFIGNAME >>Makefile-$CONFIGNAME
cat Makefile.in | sed -e "s/@GAPARCH@/$GAParchprot/g" | sed -e "s/@CONFIGNAME@/$CONFIGNAME/g"  >>Makefile-$CONFIGNAME
ln -s Makefile-$CONFIGNAME Makefile
echo "Created ./Makefile-"$CONFIGNAME" with link from ./Makefile"

back to top