aboutsummaryrefslogtreecommitdiff
path: root/etc/utils
diff options
context:
space:
mode:
authorCyril Cohen2018-04-24 15:40:01 +0200
committerCyril Cohen2018-04-24 15:40:01 +0200
commitb941b463134b62962ebca656d5906bb3bcb07395 (patch)
tree3d8a9b34ce434f880a99ae0076a529873c7132bf /etc/utils
parent591c3e4f02eee85577f3609a00c50ebc763e86cc (diff)
fix opam packager script + dependencies
Diffstat (limited to 'etc/utils')
-rwxr-xr-xetc/utils/packager4
1 files changed, 2 insertions, 2 deletions
diff --git a/etc/utils/packager b/etc/utils/packager
index d0c4b17..2bc5379 100755
--- a/etc/utils/packager
+++ b/etc/utils/packager
@@ -56,8 +56,8 @@ else
# variables useful for package construction
URLLINE="http: \"$ARCHIVEURL\""
CHECKSUMLINE="checksum: \"$SUM\""
- PKGS=$(ls -fs -d -1 $EXTRACTED/*/mathcomp/*/ \
- | sed -r "s?.*mathcomp/([^/]+)/?\1?" \
+ PKGS=$(ls -fs -d -1 $EXTRACTED/*/mathcomp/*/opam \
+ | sed -r "s?.*mathcomp/([^/]+)/opam?\1?" \
| paste -sd " " -)
PKGPREFIX="$(git root)/opam/released/packages"
fi