Update Dockerfile
This commit is contained in:
@@ -37,6 +37,7 @@ ENV VSCODE_API_VERSION="1.50.0"
|
|||||||
RUN ssh -o StrictHostKeyChecking=no github.com || true
|
RUN ssh -o StrictHostKeyChecking=no github.com || true
|
||||||
|
|
||||||
# Lean4game specific stuff
|
# Lean4game specific stuff
|
||||||
|
RUN mkdir -p /workspace
|
||||||
WORKDIR /workspace
|
WORKDIR /workspace
|
||||||
RUN git clone https://github.com/leanprover-community/lean4game.git
|
RUN git clone https://github.com/leanprover-community/lean4game.git
|
||||||
WORKDIR /workspace/lean4game
|
WORKDIR /workspace/lean4game
|
||||||
|
|||||||
Reference in New Issue
Block a user