on master help sign in
Allow Travis to work when repo isn't named Idris-dev.
1333098Steven Shaw
.travis.yml+6−2
@@ -2,6 +2,10 @@ sudo: false
2
2
3language: c
3language: c
4
4
5+env:
6+ global:
7+ - PKGNAME=idris
8+
5addons:
9addons:
6 apt:
10 apt:
7 sources:
11 sources:
@@ -113,8 +117,8 @@ install:
113before_script:
117before_script:
114 - cabal sdist
118 - cabal sdist
115 - cd ..
119 - cd ..
116− - tar -xf Idris-dev/dist/idris*.tar.gz
120+ - tar -xf */dist/${PKGNAME}*.tar.gz
117− - cd idris*
121+ - cd ${PKGNAME}*
118script:
122script:
119###
123###
120 - echo 'Configure...' && echo -en 'travis_fold:start:script.configure\\r'
124 - echo 'Configure...' && echo -en 'travis_fold:start:script.configure\\r'