From 933394bb6fb48c53d1443e8a57ac5f0488dc45ea Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 10 Nov 2023 11:16:25 +0100 Subject: [PATCH] Update running_locally.md --- doc/running_locally.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/running_locally.md b/doc/running_locally.md index 66d09cb..9ee9db5 100644 --- a/doc/running_locally.md +++ b/doc/running_locally.md @@ -85,7 +85,7 @@ git clone https://github.com/hhu-adam/GameSkeleton.git Download dependencies and build the game: ```bash cd GameSkeleton -lake update +lake update -R lake exe cache get # if your game depends on mathlib lake build ``` @@ -118,7 +118,7 @@ When modifying the game engine itself (in particular the content in `lean4game/s ```bash cd NNG4 export LEAN4GAME=local -lake update +lake update -R lake build ``` This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, when you `lake build` your game, it will rebuild with the modified `GameServer`.