From b77718fd9f6c8da3cf375e756c31fb4fe02b729f Mon Sep 17 00:00:00 2001
From: Matthias Wolf <matthias.wolf@epfl.ch>
Date: Thu, 25 Jul 2019 09:06:36 +0200
Subject: [PATCH] docker: pull in newest changes. (#451)

---
 docker/Dockerfile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/docker/Dockerfile b/docker/Dockerfile
index c04d2559c08f4c..f2922319fa993c 100644
--- a/docker/Dockerfile
+++ b/docker/Dockerfile
@@ -38,6 +38,9 @@ ARG revision=develop
 RUN if [[ "x$pr" != "x" ]]; then \
             git fetch origin +refs/pull/$pr/head:refs/remotes/origin/pull/$pr \
             && git checkout pull/$pr; \
+    elif [[ "x$revision" = "xdevelop" ]]; then \
+            git checkout $revision \
+            && git pull --ff-only; \
     else \
             git fetch \
             && git checkout $revision; \