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 Apr 10, 2024
1 parent db66cb1 commit de1ff4f
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion doc/create_game.md
Original file line number Diff line number Diff line change
Expand Up @@ -242,7 +242,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the

In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md).

## 8. Publish your game
## 8. Add translation

See [Translating a game](translate.md).

## 9. Publish your game

To publish your game on the official server, see [Publishing a game](publish_game.md)

Expand Down

0 comments on commit de1ff4f

Please sign in to comment.