From 33477fadfd9533fac08f888527c7ad3083899af2 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 20 Oct 2017 02:42:37 +0200
Subject: reproduce github archive locally rather than downloading, much faster

---
 etc/utils/packager | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'etc/utils')

diff --git a/etc/utils/packager b/etc/utils/packager
index daee789..d0c4b17 100755
--- a/etc/utils/packager
+++ b/etc/utils/packager
@@ -48,7 +48,8 @@ then
   PKGPREFIX="$(git root)/opam/extra-dev/packages"
 else
   ARCHIVE=$(mktemp)
-  wget -O $ARCHIVE $ARCHIVEURL
+  git archive --format=tgz --output=$ARCHIVE \
+      --prefix=math-comp-$TAG/ $TAG # reproduce github archive
   SUM=$(md5sum $ARCHIVE | cut -d " " -f 1)
   EXTRACTED=$(mktemp -d)
   tar -C $EXTRACTED -zxvf $ARCHIVE
@@ -81,3 +82,6 @@ do pkgdir="$PKGPREFIX/coq-mathcomp-$pkg/coq-mathcomp-$pkg.$VERSION"
    then echo $CHECKSUMLINE >> $pkgdir/url
    fi
 done
+
+# finally test the existence of the archive
+wget --spider $ARCHIVEURL
-- 
cgit v1.2.3