changeset 28555:24f43782e04c

maint: merge stable to default.
author Markus Mützel <markus.muetzel@gmx.de>
date Fri, 10 Jul 2020 08:35:35 +0200
parents eae3b1e3c6c4 (current diff) 7a17dfa7716d (diff)
children 3fe9e1009399
files
diffstat 1 files changed, 5 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/bootstrap	Fri Jul 10 00:56:22 2020 -0400
+++ b/bootstrap	Fri Jul 10 08:35:35 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
     ;;