From 0ae099414cc2c4751b0a186ef823c89295711f1b Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 13 Jun 2024 10:39:31 +0200 Subject: [PATCH] Update create_game.md --- doc/create_game.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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.