Merge branch 'ls/travis-scriptify' into next

The scripts to drive TravisCI has been reorganized and then an
optimization to avoid spending cycles on a branch whose tip is
tagged has been implemented.

* ls/travis-scriptify:
travis-ci: fix "skip_branch_tip_with_tag()" string comparison

diff --git a/ci/lib-travisci.sh b/ci/lib-travisci.sh
index 9c4ae9bdd0aa57027304425948dc32009a518f96..b3ed0a0ddac4261307a31a99f3cd18fb7aabc4fc 100755 (executable)
--- a/ci/lib-travisci.sh
+++ b/ci/lib-travisci.sh
@@ -14,7 +14,7 @@ skip_branch_tip_with_tag () {
        # of a tag.
 
        if TAG=$(git describe --exact-match "$TRAVIS_BRANCH" 2>/dev/null) &&
-               $TAG != $TRAVIS_BRANCH
+               test "$TAG" != "$TRAVIS_BRANCH"
        then
                echo "Tip of $TRAVIS_BRANCH is exactly at $TAG"
                exit 0