From b1fc37f465991aa57ae18efe043eb8b12bfc2fb7 Mon Sep 17 00:00:00 2001
From: Darshit Shah <darnir@gnu.org>
Date: Sun, 14 Jan 2018 11:33:52 +0100
Subject: [PATCH] * bootstrap: Use the faster gnulib-tool.py script if possible

---
 bootstrap | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/bootstrap b/bootstrap
index 25920e99..22db9922 100755
--- a/bootstrap
+++ b/bootstrap
@@ -688,8 +688,11 @@ if $bootstrap_sync; then
   }
 fi
 
-gnulib_tool=$GNULIB_SRCDIR/gnulib-tool
-<$gnulib_tool || exit $?
+gnulib_tool=$GNULIB_SRCDIR/gnulib-tool.py
+if ! <$gnulib_tool; then
+  gnulib_tool=$GNULIB_SRCDIR/gnulib-tool
+  <$gnulib_tool || exit $?
+fi
 
 # Get translations.