Allow Travis to work when repo isn't named Idris-dev.
commit133309841c6c670a5174c4c9b5b7f62b8f715702
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 19:31 (10 years ago)
parent51da43f
.travis.yml+6−2
@@ -2,6 +2,10 @@ sudo: false
22
33language: c
44
5+env:
6+ global:
7+ - PKGNAME=idris
8+
59addons:
610 apt:
711 sources:
@@ -113,8 +117,8 @@ install:
113117before_script:
114118 - cabal sdist
115119 - cd ..
116− - tar -xf Idris-dev/dist/idris*.tar.gz
117− - cd idris*
120+ - tar -xf */dist/${PKGNAME}*.tar.gz
121+ - cd ${PKGNAME}*
118122script:
119123###
120124 - echo 'Configure...' && echo -en 'travis_fold:start:script.configure\\r'