Skip to content

Commit

Permalink
Update create_game.md
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster authored Jun 13, 2024
1 parent b091ec5 commit 0ae0994
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/create_game.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 0ae0994

Please sign in to comment.