Skip to content

Commit

Permalink
circleci: use opam_name if defined
Browse files Browse the repository at this point in the history
  • Loading branch information
liyishuai committed May 27, 2020
1 parent 105fa3d commit e5d66fd
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion config.yml.mustache
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ jobs:
name: Test dependants
command: |
PINS=$(echo `opam list -s --pinned --columns=package` | sed 's/ /,/g')
PACKAGES=`opam list -s --depends-on coq-{{ shortname }} --coinstallable-with $PINS`
PACKAGES=`opam list -s --depends-on {{ opam_name }}{{^ opam_name }}coq-{{ shortname }}{{/ opam_name }} --coinstallable-with $PINS`
if ! [ -z "$PACKAGES" ]
then opam install -t $PACKAGES
fi
Expand Down

0 comments on commit e5d66fd

Please sign in to comment.