From d837344797233ce1d0ca0a4b2d78b77908d6451e Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 26 Apr 2023 01:52:21 +0200 Subject: [PATCH] fix --- server/server.Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/server.Dockerfile b/server/server.Dockerfile index 1128d47..00204f6 100644 --- a/server/server.Dockerfile +++ b/server/server.Dockerfile @@ -7,7 +7,7 @@ WORKDIR / COPY GameServer ./GameServer COPY Main.lean ./Main COPY lakefile.lean ./lakefile.lean -COPY lake-manifest.lean ./lake-manifest.lean +COPY lake-manifest.json ./lake-manifest.json COPY lean-toolchain ./lean-toolchain COPY $GAME_DIR ./$GAME_DIR # TODO: make `adam` a build argument