diff options
author | Jameson Graef Rollins <jrollins@finestructure.net> | 2009-11-28 18:22:58 -0500 |
---|---|---|
committer | Jameson Graef Rollins <jrollins@finestructure.net> | 2009-11-28 18:22:58 -0500 |
commit | cfa246272d61c735dd77b9a873ce477d81321c46 (patch) | |
tree | b87ba4256c08d2b4dc1da93b1402e0b0541c6b3f | |
parent | a2a522a758518d19e0cf4b96cf3c55287b0fbf4f (diff) |
fix configure script to handle --prefix= and properly create Makefile.config
This also removes the Makefile.config from the repository, since it
shouldn't be kept in the repository and should be created by the
configure script.
-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 |