Fixed CI merging from release into develop branch - Part 2

Author: Johannes Weiß

scripts/ci/building/push_new_versionnumber.sh

@@ -63,8 +63,8 @@ else
       git checkout develop
       echo "git merge release"
       git merge release
-      echo "git pull --rebase $remote develop"
-      git pull --rebase $remote develop
+      echo "git pull $remote develop"
+      git pull $remote develop
       echo "git push $remote HEAD:refs/heads/develop"
       git push $remote HEAD:refs/heads/develop