#!/bin/sh

(cd config; make -f Makefile.ini clean; make -f Makefile.ini BOOTSTRAPCFLAGS="$*")
if [ ! -f config/personal.def ]; then
    touch config/personal.def
fi
./config/imake -I./config -DUseInstalled $*

