Skip to content

Commit

Permalink
Update running_locally.md
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster authored Nov 10, 2023
1 parent e09c016 commit 933394b
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions doc/running_locally.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
Expand Down Expand Up @@ -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`.

0 comments on commit 933394b

Please sign in to comment.