diff --git a/doc/create_game.md b/doc/create_game.md index 589fc1df..3a4452e7 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -6,7 +6,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr 1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository". 2. Clone the game repo. -3. Call `lake update && lake exe cache get && lake build` to build the Lean project. +3. Call `lake update -R && lake build` to build the Lean project. Note that you need to host your game's code on github to publish it online later on. If you only want to play it locally, you can simply clone the NNG repo and start modifying that one.