configure

#!/bin/sh

######################################################################
#                                                                    #
#                           Moca                                     #
#                                                                    #
#          Pierre Weis, INRIA Rocquencourt                           #
#          Frédéric Blanqui, projet Protheo, INRIA Lorraine          #
#                                                                    #
#  Copyright 2005-2012,                                              #
#  Institut National de Recherche en Informatique et en Automatique. #
#  All rights reserved.                                              #
#                                                                    #
#  This file is distributed under the terms of the Q Public License. #
#                                                                    #
######################################################################

# $Id: configure,v 1.7 2012-06-04 13:01:22 weis Exp $

# The script to configure Makefile.config.
# i.e. to set up the value of PREFIX.

GENERATED=Makefile.config

PREFIXDIR="/usr/local"
SRCROOTDIR=

case $# in
 2) PREFIXDIR=$1; SRCROOTDIR=$2;;
 *) \
    echo "******* FATAL CONFIGURATION ERROR **********"; \
    echo "Script config/configure needs two arguments"; \
    echo "configuration failed. Please report it."; \
    exit 2;;
esac

#echo $PREFIXDIR
#echo $SRCROOTDIR

rm -f $GENERATED

echo "#" > $GENERATED
echo "# Warning: this file has been generated." >> $GENERATED
echo "#" >> $GENERATED
echo "# DO NOT EDIT THIS FILE!" >> $GENERATED
echo "#" >> $GENERATED
echo "# The editable source of this file is in $GENERATED.in" >> $GENERATED
echo "#" >> $GENERATED

sed -e "s|PREFIX=.*|PREFIX=$PREFIXDIR|" \
    -e "s|SRCROOTDIR=.*|SRCROOTDIR=$SRCROOTDIR|" \
 $GENERATED.in >> $GENERATED

chmod -w $GENERATED