From 537a1a5ab31ab9617bede3e338ca6af3f4308fb9 Mon Sep 17 00:00:00 2001 From: Michele Alberti <michele.alberti@cea.fr> Date: Wed, 6 Jul 2022 15:26:19 +0200 Subject: [PATCH] [docker] Fix some issues in the Makefile for the docker image. --- docker/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docker/Makefile b/docker/Makefile index 4ee02b8d..d721e301 100644 --- a/docker/Makefile +++ b/docker/Makefile @@ -25,14 +25,14 @@ all: Dockerfile @echo "You may want to consider adding ARGS=--no-cache to force" @echo "Docker to rebuild all layers." - docker build . -t laiser/caisar:pub -f $^ --rm + docker build . -t laiser/caisar:pub -f $^ --rm $(ARGS) push: all @echo "You may need to execute 'docker login' beforehand." docker push laiser/caisar:pub Dockerfile: Makefile Dockerfile.template env.template - sed 's|@UBUNTU_OPAM_BASE@|ocaml/opam:ubuntu-ocaml-4.13|g' Dockerfile.template | \ + sed 's|@UBUNTU_OPAM_BASE@|ocaml/opam:ubuntu-ocaml-@OCAMLV@|g' Dockerfile.template | \ sed 's|@ENV@|$(shell cat env.template)|g' | \ sed 's|@OPAM_DEPS@|conf-protoc conf-gmp conf-autoconf conf-pkg-config|' | \ sed 's|@OCAMLV@|4.13|g' | \ -- GitLab