From 1dac3cf3878b26ec2a9eb19669d7f730cdc3033a Mon Sep 17 00:00:00 2001 From: Dmitry Savintsev Date: Sat, 4 Nov 2023 21:08:04 +0100 Subject: [PATCH] fix dead documentation link --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 986e349..349e5e9 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ There are multiple ways to run the game while developing it: ### VSCode Devcontainer -The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#running-games-locally). +The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/doc/DOCUMENTATION.md#running-games-locally). In particular, the recommended setup is to have `docker` installed on your computer and then click on the pop-up "Reopen in Container" which is shown when opening this project in VSCode. @@ -33,7 +33,7 @@ As with devcontainers, you need to run `lake build` after changing any lean file ### Local setup -The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md#running-games-locally). +The full instructions are at [Running games locally](https://github.com/leanprover-community/lean4game/blob/main/doc/DOCUMENTATION.md#running-games-locally). In particular, the recommended setup is to have `docker` installed on your computer and then click on the pop-up "Reopen in Container" which is shown when opening this project in VSCode.