Commit Graph

1055 Commits (4652f6d50fc510f9ee42e2878a1a54cda12fd420)
 

Author SHA1 Message Date
Jon Eugster 4652f6d50f add support for external images in chat #235 2 years ago
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 71fad5699e turn defeq-hints on by default #45 2 years ago
Jon Eugster a7d746a8e5 add defeq-hints #45 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 b9112bfb09 add 'using' as known keyword 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 02978a38ed add allowed keywords #215 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
Jon Eugster 4e7c958348
Update client/public/locales/zh/translation.json 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 d034148bec
Update README.md 2 years ago
Jon Eugster 3d9d244b31 mark another string from translation 2 years ago
Jon Eugster feaf6dae0c
Update translate.md 2 years ago
Jon Eugster 6059ff1da7
Update translate.md 2 years ago
Jon Eugster 6f95f41d14
Update translate.md 2 years ago
Jon Eugster 335209b094
Update README.md 2 years ago
Jon Eugster de1ff4fadc
Update create_game.md 2 years ago
Jon Eugster db66cb1fcc
Create translate.md 2 years ago
Jon Eugster 66aa8e688e npm audit 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 67b03d9ccf bump to v4.7.0 2 years ago
Jon Eugster a15dd0a1bd bump i18n 2 years ago
Hydrogenbear ded9c38170 Merge remote-tracking branch 'upstream/dev' into cn-i18n 2 years ago
Jon Eugster d456621875 apply suggestions from PR #206 manually 2 years ago
Jon Eugster 74059bd5af fix typo 2 years ago