diff options
| -rw-r--r-- | Makefile.config | 3 | ||||
| -rwxr-xr-x | configure | 12 |
2 files changed, 11 insertions, 4 deletions
diff --git a/Makefile.config b/Makefile.config deleted file mode 100644 index ddc7436..0000000 --- a/Makefile.config +++ /dev/null @@ -1,3 +0,0 @@ -prefix = /usr/local -bash_completion_dir = /etc/bash_completion.d -CFLAGS += -DHAVE_VALGRIND @@ -1,5 +1,15 @@ #! /bin/sh +# defaults +PREFIX=/usr/local + +# option parsing +for option; do + if [ "${option%=*}" = '--prefix' ] ; then + PREFIX="${option#*=}" + fi +done + cat <<EOF Welcome to Notmuch, a system for indexing, searching and tagging your email. @@ -130,7 +140,7 @@ EOF # construct the Makefile.config cat > Makefile.config <<EOF -prefix = /usr/local +prefix = $PREFIX bash_completion_dir = /etc/bash_completion.d CFLAGS += ${have_valgrind} EOF |