From 3daaa87bd9f00dbf988b1a562f19770534cdb61f Mon Sep 17 00:00:00 2001
From: Thomas Letan <lthms@nomadic-labs.com>
Date: Mon, 18 Dec 2023 23:58:18 +0100
Subject: [PATCH] Docker: Copy irmin/ directory

---
 build.Dockerfile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/build.Dockerfile b/build.Dockerfile
index 0d8e1427bde6..45a4b0d44c75 100644
--- a/build.Dockerfile
+++ b/build.Dockerfile
@@ -24,6 +24,7 @@ COPY --chown=tezos:nogroup script-inputs/dev-executables tezos/script-inputs/
 COPY --chown=tezos:nogroup dune tezos
 COPY --chown=tezos:nogroup scripts/version.sh tezos/scripts/
 COPY --chown=tezos:nogroup src tezos/src
+COPY --chown=tezos:nogroup irmin tezos/irmin
 COPY --chown=tezos:nogroup etherlink tezos/etherlink
 COPY --chown=tezos:nogroup tezt tezos/tezt
 COPY --chown=tezos:nogroup opam tezos/opam
-- 
GitLab