# HG changeset patch
# User Markus Mützel <markus.muetzel@gmx.de>
# Date 1594362873 -7200
# Node ID 7a17dfa7716db374bf7dac34f171ad34c6b52478
# Parent  aa47120a505daab48848b94f73d0625db8724034
bootstrap: Merge back local changes removed in f00e92f9e85b.

diff -r aa47120a505d -r 7a17dfa7716d bootstrap
--- a/bootstrap	Fri Jul 10 00:31:10 2020 -0400
+++ b/bootstrap	Fri Jul 10 08:34:33 2020 +0200
@@ -670,6 +670,11 @@
         || cleanup_gnulib
 
       trap - 1 2 13 15
+
+    elif test -n "$GNULIB_REVISION" \
+         && ! git --git-dir="$gnulib_path"/.git cat-file \
+              commit "$GNULIB_REVISION"; then
+      git --git-dir="$gnulib_path"/.git fetch
     fi
     GNULIB_SRCDIR=$gnulib_path
     ;;