docker: pull in newest changes. (BlueBrain#451)

lguyot · Jul 25, 2019 · b77718f · b77718f
1 parent 7da86ca
commit b77718f
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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; \