diff --git a/tools/build-system/launch-build-machine-jenkins.sh b/tools/build-system/launch-build-machine-jenkins.sh
index 771f222c6e660b4186208c10cba06faaadbda659..04634715a3d9eb1a3d917a00e1e2824eaf5c0efc 100755
--- a/tools/build-system/launch-build-machine-jenkins.sh
+++ b/tools/build-system/launch-build-machine-jenkins.sh
@@ -116,7 +116,7 @@ echo "Update reference sources"
 git checkout . && git checkout -f master && git pull
 
 # Get the version
-if [ -n $TAG ]; then
+if [ -n "$TAG" ]; then
     CURRENT_RELEASE_TAG_NAME="$TAG"
 else
     CURRENT_RELEASE_TAG_NAME=`git describe --tags --abbrev=0`