use LOCAL.config

This commit is contained in:
rsc 2005-02-02 22:08:10 +00:00
parent 41e0f84ca6
commit 52fdc1a547

View file

@ -4,7 +4,7 @@ PLAN9=`pwd` export PLAN9
PATH=$PLAN9/bin:$PATH export PATH
echo "Resetting $PLAN9/config"
rm -f $PLAN9/config
rm -f config
(
if [ `uname` = Linux ]; then
@ -23,6 +23,13 @@ if [ `uname` = Linux ]; then
fi
rm -f ./a.out
fi
if [ -f LOCAL.config ]; then
echo Using LOCAL.config options:
sed 's/^/ /' LOCAL.config
cat LOCAL.config >>config
fi
echo "Building mk..."
cd src
make