diff --git a/devel_tools/docker/frama-c.custom/Dockerfile b/devel_tools/docker/frama-c.custom/Dockerfile index 226b19fcf0030a9d07c9f7dfba2705e082986256..c742082bbd45bb69371125d868de56357da68e84 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