Update create_game.md

This commit is contained in:
Jon Eugster
2023-11-09 16:54:06 +01:00
committed by GitHub
parent 335e7e6883
commit ebcde9d588
+1 -1
View File
@@ -4,7 +4,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr
## 1. Create the project
1. Use the [NNG template](https://github.com/hhu-adam/NNG4) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository".
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.