From dae191720c4b1b31dd4e58bc01819bfebcb403ec Mon Sep 17 00:00:00 2001
From: Nils Wentzell <nils.wentzell@gmail.com>
Date: Tue, 13 Mar 2018 13:29:43 +0100
Subject: [PATCH] [doc] Updating jenkins and dockerfile after previous commit

---
 Dockerfile  | 4 ++--
 Jenkinsfile | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Dockerfile b/Dockerfile
index 299f2e60..6b28ea52 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -5,7 +5,7 @@ COPY . ${SRC}/dft_tools
 WORKDIR ${BUILD}/dft_tools
 RUN chown build .
 USER build
-ARG BUILD_DOC=0
-RUN cmake ${SRC}/dft_tools -DTRIQS_ROOT=${INSTALL} -DBUILD_DOC=${BUILD_DOC} && make -j2 && make test
+ARG Build_Documentation=0
+RUN cmake ${SRC}/dft_tools -DTRIQS_ROOT=${INSTALL} -DBuild_Documentation=${Build_Documentation} && make -j2 && make test
 USER root
 RUN make install
diff --git a/Jenkinsfile b/Jenkinsfile
index d57884a3..9274b8d0 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -28,7 +28,7 @@ for (int i = 0; i < dockerPlatforms.size(); i++) {
         mv -f Dockerfile.jenkins Dockerfile
       """
       /* build and tag */
-      def img = docker.build("flatironinstitute/${projectName}:${env.BRANCH_NAME}-${env.STAGE_NAME}", "--build-arg BUILD_DOC=${platform==documentationPlatform} .")
+      def img = docker.build("flatironinstitute/${projectName}:${env.BRANCH_NAME}-${env.STAGE_NAME}", "--build-arg Build_Documentation=${platform==documentationPlatform} .")
       if (env.BRANCH_NAME.startsWith("PR-") || platform != documentationPlatform) {
         /* but we don't need the tag so clean it up (except for documentation) */
         sh "docker rmi ${img.imageName()}"