diff --git a/Makefile.config b/Makefile.config deleted file mode 100644 index ddc74365..00000000 --- a/Makefile.config +++ /dev/null @@ -1,3 +0,0 @@ -prefix = /usr/local -bash_completion_dir = /etc/bash_completion.d -CFLAGS += -DHAVE_VALGRIND diff --git a/configure b/configure index e55f067e..ab28fa30 100755 --- a/configure +++ b/configure @@ -1,5 +1,15 @@ #! /bin/sh +# defaults +PREFIX=/usr/local + +# option parsing +for option; do + if [ "${option%=*}" = '--prefix' ] ; then + PREFIX="${option#*=}" + fi +done + cat < Makefile.config <