From 857d2db3339d1bb7ef2e32c2d84f98aad88532c6 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 21 Sep 2020 14:28:04 +0200
Subject: [PATCH] Do not remove sources in the docker image when compilation
fails
---
devel_tools/docker/frama-c.custom/Dockerfile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/devel_tools/docker/frama-c.custom/Dockerfile b/devel_tools/docker/frama-c.custom/Dockerfile
index 226b19fcf00..c742082bbd4 100644
--- a/devel_tools/docker/frama-c.custom/Dockerfile
+++ b/devel_tools/docker/frama-c.custom/Dockerfile
@@ -47,7 +47,7 @@ RUN cd /root && \
make -j && \
make install \
) && \
- [ "${with_source}" != "no" ] || rm -rf frama-c
+ ([ "${with_source}" != "no" ] || rm -rf frama-c)
# with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no
--
GitLab