CI: fix in merge from develop-ci

Signed-off-by: Raphael Defosseux <raphael.defosseux@eurecom.fr>
2018-06-25 13:46:32 +02:00
parent bee199735f
commit 0b0f70bc48
2 changed files with 10 additions and 0 deletions
@@ -81,6 +81,16 @@ case $key in
    usage
    exit 0
    ;;
    -jn|--job-name)
    JOB_NAME="$2"
    shift
    shift
    ;;
    -id|--build-id)
    BUILD_ID="$2"
    shift
    shift
    ;;
    -ws|--workspace)
    JENKINS_WKSP="$2"
    shift