You cannot select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
lean4game/doc/publish_game.md

30 lines
1003 B
Markdown

1 year ago
# Publishing games
1 year ago
You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple
steps.
1 year ago
## 1. Upload Game to github
1 year ago
First, you need your game in a public Github repository and make sure the github action has run.
You can check this by spotting the green checkmark on the start page, or by looking at the "Actions"
tab.
1 year ago
## 2. Import the game
1 year ago
You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call
the URL of the form
1 year ago
> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}
1 year ago
where `{USER}` and `{REPOSITORY}` are replaced with the github user and repository name.
1 year ago
You should see a white screen which shows import updates and eventually reports "Done."
## 3. Play the game
Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`!
## 4. Main page
Adding games to the main page happens manually by the server maintainers. Tell us if youwould like your game to appear on the start page.