From a46107ba7f8fa6f7d204338dce33e2319d6148d0 Mon Sep 17 00:00:00 2001
From: Martin Diehl <m.diehl@mpie.de>
Date: Fri, 14 Apr 2017 09:16:21 +0200
Subject: [PATCH] pull needed to avoid conflicts

---
 .gitlab-ci.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 72728cebe..2767c46dd 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -435,6 +435,7 @@ mergeIntoMaster:
     - git merge $UPDATEDREV
     - git push origin master                                                                        # master is now tested version and has updated VERSION file
     - git checkout development
+    - git pull
     - git merge master -s ours                                                                      # only possible conflict is in VERSION file
     - git push origin development                                                                   # development is unchanged (as master is based on it) but has updated VERSION file
   only: