From c2f77d08fb15feb5f0f5826c55fa525f3659d986 Mon Sep 17 00:00:00 2001
From: Matthias Andreas Benkard <code@mail.matthias.benkard.de>
Date: Wed, 7 Dec 2011 20:27:10 +0100
Subject: Add the option of configuring the BPT key and bitmask sizes.

---
 configure | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100755 configure

(limited to 'configure')

diff --git a/configure b/configure
new file mode 100755
index 0000000..7e9d15e
--- /dev/null
+++ b/configure
@@ -0,0 +1,25 @@
+#! /bin/sh
+
+if [ sed --version >/dev/null 2>&1 ]; then
+  GSED=sed
+else
+  GSED=gsed
+fi
+
+if [ "$#" -lt 2 ]; then
+  echo "Usage:"
+  echo "  ./configure <bpt_key_t> <bpt_key_bitmask_t>"
+  echo
+  echo "Example:"
+  echo "  ./configure intptr_t int64_t"
+  exit 2
+fi
+
+KEY_T=$1
+BITMASK_T=$2
+
+make config ADDITIONAL_CFLAGS="-DBPT_KEY_T=$KEY_T -DBPT_KEY_BITMASK_T=$BITMASK_T"
+CONFIG_CFLAGS=$(./config)
+make clean
+
+"$GSED" --in-place "s/ADDITIONAL_CFLAGS =.*\$/ADDITIONAL_CFLAGS = $CONFIG_CFLAGS -DBPT_EXPLICIT_CONFIGURATION -DBPT_KEY_T=$KEY_T -DBPT_KEY_BITMASK_T=$BITMASK_T/" Makefile
-- 
cgit v1.2.3