From d71a0b60520b5070532e5fa9031b46b0e413e241 Mon Sep 17 00:00:00 2001
From: Jan Nieuwenhuizen <janneke@gnu.org>
Date: Sun, 4 Nov 2018 19:14:52 +0100
Subject: [PATCH] gash: WIP

---
 configure.sh | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/configure.sh b/configure.sh
index ae6aa726..aae9b7c9 100755
--- a/configure.sh
+++ b/configure.sh
@@ -18,20 +18,18 @@
 # You should have received a copy of the GNU General Public License
 # along with GNU Mes.  If not, see <http://www.gnu.org/licenses/>.
 
-set -e
+set -ex
 
 VERSION=0.18
 
 # parse --prefix=prefix
 cmdline=$(echo "$@")
-p=${cmdline##*--prefix=}
-p=${p% *}
-p=${p% -*}
+p=$(echo "$@" | grep -o '[-][-]prefix=[^ ]*')
+p=$(echo "$p" | sed -e 's,--prefix=,,')
 if [ -z "$p" ]; then
     p=${prefix-/usr/local}
 fi
 prefix=$p
-
 srcdir=${srcdir-$(dirname $0)}
 . ${srcdest}build-aux/trace.sh