search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

feat: allow for custom translations #237

Open joneugster opened 5 months ago

joneugster commented 5 months ago

We might want to allow games to provide there custom translations of the interface.

See e.g. https://github.com/hhu-adam/Robo/issues/47 which asks to replace "World" by "Planet"

TentativeConvert commented 5 months ago

Alternatively, we could try to be agnostic and hard-code as little text as possible. Why do we need "World:" at the top of the screen to begin with? (And "World overview" in the menu could be "Game overview".)

joneugster commented 5 months ago

You're right, we don't need it. Changed the "world overview" to "Home" and removed the word "world" in other places.

The only appearance of "world" is now on the games' tiles on the landing page.