From e914afb412e8112ebf260a1000fde8ab1d91517a Mon Sep 17 00:00:00 2001
From: Christian Grothoff <christian@grothoff.org>
Date: Tue, 1 Oct 2019 13:55:23 +0200
Subject: [PATCH] pass all arguments

---
 configure | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/configure b/configure
index 7f5bf251b..c03fc63ad 100755
--- a/configure
+++ b/configure
@@ -115,4 +115,4 @@ chmod +x configure.py
 # If $1 is empty, the python script checks the
 # environment for PREFIX. We might need more
 # variables and switches, such as DESTDIR.
-./configure.py "$1"
+./configure.py $@