[deployment] do not upload a PR as dev version

gph82 · Jun 7, 2016 · 69298ed · 69298ed
1 parent 8e5cdd7
commit 69298ed
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/devtools/ci/travis/after_success.sh b/devtools/ci/travis/after_success.sh
@@ -1,9 +1,12 @@
 #!/bin/bash
-if [ "$TRAVIS_PULL_REQUEST" = true ]; then
+
+# The pull request number if the current job is a pull request, “false” if it’s not a pull request.
+if [[ ! "$TRAVIS_PULL_REQUEST" == "false" ]]; then
     echo "This is a pull request. No deployment will be done."; exit 0
 fi
 
-
+# For builds not triggered by a pull request this is the name of the branch currently being built;
+# whereas for builds triggered by a pull request this is the name of the branch targeted by the pull request (in many cases this will be master).
 if [ "$TRAVIS_BRANCH" != "devel" ]; then
     echo "No deployment on BRANCH='$TRAVIS_BRANCH'"; exit 0
 fi