1 files changed, 8 insertions, 1 deletions
diff --git a/INSTALL b/INSTALL
index c0c04db2..650cd8f2 100755
--- a/INSTALL
+++ b/INSTALL
@@ -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