Commit Graph

466 Commits (f1582503418a80cb9afb81cc94b2a636b02c52e0)

Author SHA1 Message Date
Jon Eugster f158250341 improve chat scrolling #82 2 years ago
Jon Eugster 7dc0a507ed fix css 2 years ago
Jon Eugster 80d4b88f5a mostly remove 'world' as a word #237 2 years ago
Jon Eugster 714b4f45b1 redefine chat scrolling #230 2 years ago
Jon Eugster 6da902aede cleanup chat css 2 years ago
Jon Eugster cdffe03f9a cleanup chat 2 years ago
Jon Eugster adeed03da8 cleanup; including cleaning up chat 2 years ago
Jon Eugster 8e3dfdea30 wip 2 years ago
Jon Eugster c735211cd8 cleanup 2 years ago
Jon Eugster 369b77f00f add search parameter to set language #220 2 years ago
Jon Eugster 895c71dc91 cleanup 2 years ago
Jon Eugster 8b5d6ff2f3 improve language selection 2 years ago
Jon Eugster c1642cf09b cleanup: popups 2 years ago
Jon Eugster d82ef8af8f refactor: navigation and other stuff 2 years ago
Jon Eugster 08875e4415 style error page 2 years ago
Jon Eugster 5765c78a1d add submenu for inventory categories 2 years ago
Jon Eugster 05fbee9365 mark inventory item from the last level 2 years ago
Jon Eugster 1daef0d80f show exercise name even if no text present 2 years ago
Jon Eugster 06cc52bb7e mark tabs with new theorems 2 years ago
Jon Eugster eac945e7b5 update impressum & privacy policy 2 years ago
Jon Eugster a1b1a33a9b remove more flags #208 2 years ago
Jon Eugster 8cf358e17b add config option to disable flags in preferences #208 2 years ago
Jon Eugster 3ddcc35137
Merge pull request #206 from JiechengZhao/cn-i18n
add Chinese translation
2 years ago
Hydrogenbear 237371a77f Merge branch 'main' of https://github.com/leanprover-community/lean4game into cn-i18n 2 years ago
Jon Eugster f308e1ad49 fix CSS of tooltips #207 2 years ago
Jon Eugster 62f1fb87d1 add numpad-enter key #212 2 years ago
Hydrogenbear c5df85ce66 Add a missed translation 2 years ago
Jon Eugster 848b2cddc8 fix hhu-adam/Robo#22 2 years ago
Jon Eugster 3d9d244b31 mark another string from translation 2 years ago
Jon Eugster a523bab1d6 fix css warning 2 years ago
Jon Eugster 499bb00d4f fix language loading on landing page 2 years ago
Jon Eugster d456621875 apply suggestions from PR #206 manually 2 years ago
Jon Eugster a8d3169ebb add some translation keys 2 years ago
Jon Eugster 9b05a27888 use translation of level title 2 years ago
Jon Eugster 5a768c25b7 mark two more translations 2 years ago
Jon Eugster 39be34e83a improve landing page 2 years ago
Jon Eugster 684a1bc72b fix initial translation loading on starting page 2 years ago
Jon Eugster 10391b616c add chinese translations 2 years ago
Jon Eugster aaa6c3b576 add german translations 2 years ago
Jon Eugster d60dc3fcb2 mark most of the game text for translation 2 years ago
Jon Eugster 1a54edffd4 bump lean-i18n and other stuff 2 years ago
Jon Eugster ad1add5264 support translations of the games 2 years ago
Jon Eugster a26022e3fc fix css 2 years ago
Jon Eugster 7c44d49b2a images on all levels 2 years ago
Jon Eugster a7784ef66b center github icon 2 years ago
Jon Eugster 389e120117 add translations 2 years ago
Jon Eugster ee9fd18a56 use global configs in i18n-scanner 2 years ago
Jon Eugster 8b29f88407 use flags for game tiles 2 years ago
Jon Eugster ebda6cc162 more progress on internationalisation 2 years ago
Jon Eugster 7e9514fe96 mark all texts for translation #179 2 years ago