From 09bf2fae0e348283535034da558e6feea93e6cfb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Hinderer?= <Sebastien.Hinderer@inria.fr>
Date: Thu, 17 May 2018 15:07:10 +0200
Subject: [PATCH] configure should remove hashbang4

---
 configure | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/configure b/configure
index 08892e638..d5165d8f5 100755
--- a/configure
+++ b/configure
@@ -1155,6 +1155,8 @@ else
   config HASHBANGSCRIPTS "false"
 fi
 
+rm hashbang4
+
 # Use 64-bit file offset if possible
 
 common_cppflags="$common_cppflags -D_FILE_OFFSET_BITS=64"