Skip to content

Update Game.pot & translation files #171

Description

@TentativeConvert

I noticed while preparing #170 that:

  • There are already a number of commits that are not reflected in Game.pot.
  • The existing po-files have not been updated to the new lean-i18n format in which latex and lean snippets get replaced by placeholders. At least the msgid's in these po-files need to be updated.

Therefore, I haven't included an updated Game.pot file in #170, nor updated json files. But these updates need to happen before the current version gets deployed.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions