remove flags from language selector

leanprover-community / lean4game

Server to host lean games.

https://adam.math.hhu.de

GNU General Public License v3.0

137 stars 25 forks source link

remove flags from language selector #208

Closed TentativeConvert closed 2 months ago

TentativeConvert commented 3 months ago

As much as I like the graphical appeal of the flags, representing languages by flags is bound to create controversies sooner or later. I would prefer to avoid them.

joneugster commented 2 months ago

We have two places we use the flags:

Preferences to select the language
On the tiles, to represent the languages of a game.

I put the former behind an option that is turned off by default. However, I kept the latter, as on the game Tiles there is only very limited space and they are all about providing information about the game in a concise and graphical way.

We can re-open this issue if there are better suggestions!

lean4game_flags

TentativeConvert commented 2 months ago

@joneugster: I guess one could use the 2 letter ISO language codes. But if you don't mind German being represented by Schwarz-Rot-Gold, I won’t insist.

joneugster commented 2 months ago

It didn't strike me particularly problematic, and I think flags for languages is something quite common online. Let's change to ISO codes then:

languages_lean4game_2

Makes it also easier if somebody wants to translate a game to latin ;)

For German, I think the choice is quite natural. The only three options are: 🇩🇪, 🇦🇹, 🇱🇮; and I think it's fair to assume that it shouldn't be Liechtenstein. (Switzerland has 4 official languages, 3 of which are equally important. so 🇨🇭 is not of any use anyways.)