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.
---
Makefile.config | 3 ---
configure | 12 +++++++++++-
2 files changed, 11 insertions(+), 4 deletions(-)
delete mode 100644 Makefile.config
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
diff --git a/configure b/configure
index e55f067..ab28fa3 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 <<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
--
1.6.5
