changeset 28014:0b67847e4f97

maint: merge stable to default.
author John W. Eaton <jwe@octave.org>
date Mon, 27 Jan 2020 10:14:36 -0500
parents 9a965fec21c1 (current diff) 717e3780805c (diff)
children 6948260b8fcf
files
diffstat 1 files changed, 5 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/bootstrap	Sun Jan 26 23:07:45 2020 -0500
+++ b/bootstrap	Mon Jan 27 10:14:36 2020 -0500
@@ -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 pull
     fi
     GNULIB_SRCDIR=$gnulib_path
     ;;