Update running_locally.md

pull/153/head
Jon Eugster 3 years ago committed by GitHub
parent e09c016c4c
commit 933394bb6f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

@ -85,7 +85,7 @@ git clone https://github.com/hhu-adam/GameSkeleton.git
Download dependencies and build the game: Download dependencies and build the game:
```bash ```bash
cd GameSkeleton cd GameSkeleton
lake update lake update -R
lake exe cache get # if your game depends on mathlib lake exe cache get # if your game depends on mathlib
lake build lake build
``` ```
@ -118,7 +118,7 @@ When modifying the game engine itself (in particular the content in `lean4game/s
```bash ```bash
cd NNG4 cd NNG4
export LEAN4GAME=local export LEAN4GAME=local
lake update lake update -R
lake build 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`. 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`.

Loading…
Cancel
Save