Skip to content

Commit

Permalink
update README to mention gitpod and codespaces
Browse files Browse the repository at this point in the history
  • Loading branch information
kbuzzard committed Aug 7, 2023
1 parent 46dd165 commit ed1aa6c
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,10 @@ If you want to contribute to the Natural Number Game, it is probably best if you

See the [documentation](https://github.com/leanprover-community/lean4game/blob/main/DOCUMENTATION.md) for an explanation of the game commands.

## Codespaces and Gitpod

You can edit this repository using Gitpod : [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/hhu-adam/NNG4) or Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main").

### Creating a new game

In order to create a new game, click "use this template" above to create your own game. That way there is a github action that can build a docker image from your `main` branch which can be used to add the game to the server at [adam.math.hhu.de](https://adam.math.hhu.de).
Expand Down

0 comments on commit ed1aa6c

Please sign in to comment.