From 8f6fb7818c5cfd279248c6f39b529f4a9f08c194 Mon Sep 17 00:00:00 2001
From: Tim Neumann <neumantm@fius.informatik.uni-stuttgart.de>
Date: Mon, 4 May 2020 22:16:09 +0200
Subject: [PATCH] Fix small syntax error in versionBump script

---
 scriptsAndTools/versionBump.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scriptsAndTools/versionBump.sh b/scriptsAndTools/versionBump.sh
index 6d60e7cec..14a049ed3 100755
--- a/scriptsAndTools/versionBump.sh
+++ b/scriptsAndTools/versionBump.sh
@@ -21,7 +21,7 @@ fi
 
 git fetch
 
-if ! [ git diff HEAD FETCH_HEAD --exit-code > /dev/null ] ;then
+if ! git diff HEAD FETCH_HEAD --exit-code > /dev/null ;then
   fail "Branch is not up to date." 9
 fi