From a20dc91fc30749aca313649a901b73e96095aba6 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 10 Sep 2023 22:11:54 +0200 Subject: [PATCH] Update Dockerfile --- .docker/gitpod/Dockerfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.docker/gitpod/Dockerfile b/.docker/gitpod/Dockerfile index 1a3a7e3..1a087ed 100644 --- a/.docker/gitpod/Dockerfile +++ b/.docker/gitpod/Dockerfile @@ -37,9 +37,9 @@ ENV VSCODE_API_VERSION="1.50.0" RUN ssh -o StrictHostKeyChecking=no github.com || true # Lean4game specific stuff -WORKDIR /home/gitpod +WORKDIR /workspace RUN git clone https://github.com/leanprover-community/lean4game.git -WORKDIR /home/gitpod/lean4game +WORKDIR /workspace/lean4game RUN npm install # run sudo once to suppress usage info