Merge remote-tracking branch 'origin/master'

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 developers
+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.

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