diff options
Diffstat (limited to 'dist')
| -rwxr-xr-x | dist/linux/travis-ci.sh | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dist/linux/travis-ci.sh b/dist/linux/travis-ci.sh index 727d28b3b..21e68790f 100755 --- a/dist/linux/travis-ci.sh +++ b/dist/linux/travis-ci.sh @@ -29,7 +29,11 @@ PKG_SHORTCOMMIT="$(printf $TRAVIS_COMMIT | cut -c1-10)" PKG_VER=`grep Ghdl_Ver src/version.in | sed -e 's/.*"\(.*\)";/\1/'` PKG_TAG="$TRAVIS_TAG" if [ -z "$TRAVIS_TAG" ]; then + # No tag: use date + commit id PKG_TAG="$(date -u +%Y%m%d)-$PKG_SHORTCOMMIT"; +elif expr "$TRAVIS_TAG" : 'v[0-9].*'; then + # Remove leading 'v' in tags in the filenames. + PKG_TAG="$(echo $TAVIS_TAG | cut -c2-)" fi if [ "$IMAGE" = "" ]; then |