From d53b57a764a44694ebceae7d1901b85b469b2e8e Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 13 Jun 2024 11:45:33 +0200 Subject: [PATCH] Update create_game.md --- doc/create_game.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/doc/create_game.md b/doc/create_game.md index 707dd3d..b26a06d 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -10,8 +10,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr ### Running the game -Now you can open the game in VSCode (`cd YourGame/` and `code .`), and start modifying it like a regular Lean project. To run the game consult -[Running Games Locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md). +Now you can open the game in VSCode (`cd YourGame/` and `code .`), and start modifying it like a regular Lean project. To run the game consult the section " 5.Testing the Game Locally" below. ## 2. Game.lean