diff options
Diffstat (limited to 'etc/utils')
| -rwxr-xr-x | etc/utils/packager | 4 |
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 |