From 85c894e5e84ac0c6abe73b5c654ed270dc4a1e6d Mon Sep 17 00:00:00 2001
From: Tim Neumann <neumantm@fius.informatik.uni-stuttgart.de>
Date: Mon, 4 May 2020 21:49:36 +0200
Subject: [PATCH 1/3] Improve versionBump script

---
 scriptsAndTools/versionBump.sh | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/scriptsAndTools/versionBump.sh b/scriptsAndTools/versionBump.sh
index 9090b248e..6d60e7cec 100755
--- a/scriptsAndTools/versionBump.sh
+++ b/scriptsAndTools/versionBump.sh
@@ -19,6 +19,12 @@ if [ "$(git branch --show-current)" != "master" ] ;then
   fail "Not on master branch." 4
 fi
 
+git fetch
+
+if ! [ git diff HEAD FETCH_HEAD --exit-code > /dev/null ] ;then
+  fail "Branch is not up to date." 9
+fi
+
 if ! [ -e "pom.xml" ] ;then
   fail "No pom detcted, Are you in root of repo?" 5
 fi

From 04851c6d5123a5ccb12a7876af202cd0662656ca Mon Sep 17 00:00:00 2001
From: Tim Neumann <neumantm@fius.informatik.uni-stuttgart.de>
Date: Mon, 4 May 2020 21:49:48 +0200
Subject: [PATCH 2/3] Add some doku about scripts and tools.

---
 scriptsAndTools/README.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 scriptsAndTools/README.md

diff --git a/scriptsAndTools/README.md b/scriptsAndTools/README.md
new file mode 100644
index 000000000..b28d9cedc
--- /dev/null
+++ b/scriptsAndTools/README.md
@@ -0,0 +1,16 @@
+# Scripts and Tools
+
+Many of these scripts expect to be run from the root directory of this folder.
+So use `$ ./scriptsAndTools/<script>.sh`
+
+Most scripts will fail if an argument is missing
+
+## Scripts to be used by developpers
+Don't use the other scripts, except if you know what you are doing.
+
+| Name | Description |
+| --- | --- |
+| `verifyFormat.sh` | Checks all format requirements. `mvn clean install` before using it.
+| `fixSourceFileHeaders.sh` | Replaces the first part of each java file in the repo with the correctHeader.
+| `formatPoms.sh` | Formats the poms according to the requirements.
+| `versionBump.sh` | Initiate a version bump and release.

From 0fdd69f3d4ba8f280781b499dd420b27d0891f85 Mon Sep 17 00:00:00 2001
From: Tim Neumann <neumantm@fius.informatik.uni-stuttgart.de>
Date: Mon, 4 May 2020 21:51:42 +0200
Subject: [PATCH 3/3] Fix typo

---
 scriptsAndTools/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scriptsAndTools/README.md b/scriptsAndTools/README.md
index b28d9cedc..aae209608 100644
--- a/scriptsAndTools/README.md
+++ b/scriptsAndTools/README.md
@@ -5,7 +5,7 @@ So use `$ ./scriptsAndTools/<script>.sh`
 
 Most scripts will fail if an argument is missing
 
-## Scripts to be used by developpers
+## Scripts to be used by developers
 Don't use the other scripts, except if you know what you are doing.
 
 | Name | Description |