Skip to content

Commit

Permalink
finmap has been released (#32)
Browse files Browse the repository at this point in the history
* finmap has been released in extra-dev
  • Loading branch information
CohenCyril authored Apr 25, 2020
1 parent b4b1486 commit a84feda
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .travis.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ install:
- docker pull ${DOCKERIMAGE}
- docker tag ${DOCKERIMAGE} ci:current
- docker run --env=OPAMYES --init -id --name=CI -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB} -w /home/coq/${CONTRIB} ci:current
- docker exec CI /bin/bash --login -c "cd ..; curl -LO https://github.com/math-comp/finmap/archive/1.5.0.tar.gz; tar -xvzf 1.5.0.tar.gz; cd finmap-1.5.0/; opam pin add -y -n coq-mathcomp-finmap.1.5.0 .; opam install coq-mathcomp-finmap.1.5.0; cd /home/coq/${CONTRIB}" # remove this line when finmap-1.5.0 is merged in opam coq archive
- docker exec CI /bin/bash --login -c "opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev"
- docker exec CI /bin/bash --login -c "opam pin add -n coq-mathcomp-${CONTRIB} ."
- docker exec CI /bin/bash --login -c "opam install --deps-only coq-mathcomp-${CONTRIB}"

Expand Down

0 comments on commit a84feda

Please sign in to comment.