diff options
| author | Cyril Cohen | 2020-04-15 18:49:51 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-04-15 18:49:51 +0200 |
| commit | 709756f9bbb92b5e5844e0133627271c974a11c2 (patch) | |
| tree | 440b00eb211876e54070966504d6a8acbf7f85c0 /etc/utils | |
| parent | ab54764c15886289107ec43b94bc355ada662c4c (diff) | |
fix packager
Diffstat (limited to 'etc/utils')
| -rwxr-xr-x | etc/utils/packager | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/etc/utils/packager b/etc/utils/packager index 9a83647..da7bddd 100755 --- a/etc/utils/packager +++ b/etc/utils/packager @@ -49,8 +49,9 @@ then PKGPREFIX="$GITROOT/opam/extra-dev/packages" else ARCHIVE=$(mktemp) + PREFIX=$(echo math-comp-$TAG | sed "s/\+/-/") git archive --format=tgz --output=$ARCHIVE \ - --prefix=math-comp-$TAG/ $TAG # reproduce github archive + --prefix=$PREFIX/ $TAG # reproduce github archive SUM=$(sha256sum $ARCHIVE | cut -d " " -f 1) EXTRACTED=$(mktemp -d) tar -C $EXTRACTED -zxvf $ARCHIVE |