phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,052 Commits 19 Branches 10 Tags
dc6f7b2822bb322b80bc4d5906893e98cda695fc
Commit Graph
386 Commits
Author SHA1 Message Date
Jon Eugster 6a8abf41bd implement stats script 2024-09-29 14:02:56 +02:00
Jon Eugster 1466a41169 fix fetch url for stats 2024-09-29 12:43:51 +02:00
Jon Eugster 3cdb9a026b fix stats 2024-09-29 12:39:09 +02:00
Jon Eugster ebd7268421 feat: add option to display server capacity 2024-09-26 18:07:25 +02:00
Jon Eugster 499bb00d4f fix language loading on landing page 2024-04-10 14:43:30 +02:00
Jon Eugster d456621875 apply suggestions from PR #206 manually 2024-04-09 09:47:05 +02:00
Jon Eugster a8d3169ebb add some translation keys 2024-04-06 15:25:31 +02:00
Jon Eugster 9b05a27888 use translation of level title 2024-04-06 14:56:19 +02:00
Jon Eugster 5a768c25b7 mark two more translations 2024-03-29 12:34:57 +01:00
Jon Eugster 39be34e83a improve landing page 2024-03-29 12:27:14 +01:00
Jon Eugster 684a1bc72b fix initial translation loading on starting page 2024-03-29 12:16:36 +01:00
Jon Eugster d60dc3fcb2 mark most of the game text for translation 2024-03-27 02:03:05 +01:00
Jon Eugster ad1add5264 support translations of the games 2024-03-27 00:22:51 +01:00
Jon Eugster 7c44d49b2a images on all levels 2024-03-26 17:24:53 +01:00
Jon Eugster 389e120117 add translations 2024-03-26 02:49:48 +01:00
Jon Eugster 8b29f88407 use flags for game tiles 2024-03-26 01:02:23 +01:00
Jon Eugster ebda6cc162 more progress on internationalisation 2024-03-26 00:30:55 +01:00
Jon Eugster 7e9514fe96 mark all texts for translation #179 2024-03-25 23:51:19 +01:00
Jon Eugster 3ac8fdace7 mark translations in app-bar 2024-03-25 22:30:55 +01:00
Jon Eugster 8d0493acb5 make preferences work #179 2024-03-25 22:23:03 +01:00
Jon Eugster 45bc0468df implement i18next and i18next-scanner 2024-03-24 17:37:31 +01:00
Jon Eugster c24efb1377 Merge pull request #203 from JiechengZhao/main 
add next_i18n
 2024-03-23 13:25:18 +01:00
Jon Eugster a9447a70d4 add interface buttons for i18n #179 2024-03-23 01:11:42 +01:00
Jon Eugster ce9f5c7840 fix locked editor mode 2024-03-22 18:11:14 +01:00
Hydrogenbear cb711205a2 Add react_i18n 2024-03-21 18:11:17 +08:00
Jon Eugster f42829422d delete hidden hints in chat on Retry 2024-03-15 18:38:32 +01:00
Jon Eugster 47297e4194 temporary fix to improve message on server crash 2024-03-11 17:33:06 +01:00
Jon Eugster f3f077741d fix client breaking if server timed out. 2024-03-11 12:33:47 +01:00
Jon Eugster edf1085310 fix ts warnings 2024-03-11 12:18:30 +01:00
Jon Eugster 68f84a3426 fix replacement for 2+ variables 2024-02-29 16:53:35 +01:00
Jon Eugster 2649f985fa plug-in variables in hints client-side 2024-02-16 16:50:10 +01:00
Jon Eugster 3775ad98c8 level completed message in editor 2024-02-14 18:36:19 +01:00
Jon Eugster c0acde14e2 hints and diags in editor 2024-02-14 15:02:14 +01:00
Jon Eugster 976d1c6901 fix: goal in editor didnt show 2024-02-14 14:53:10 +01:00
Jon Eugster 3998fb2fc9 Merge branch 'main' into dev 2024-02-07 12:51:39 +01:00
Jon Eugster 6aebb8993f update proof from editor 2024-02-07 12:50:39 +01:00
Jon Eugster 6472ef5b31 First big junk of communication refactor 2024-02-07 12:50:39 +01:00
Jon Eugster 3b660c5185 Merge branch 'dev'. Bump to v4.5.0 2024-02-02 12:44:32 +01:00
ran 9d4a6df139 Remove MobileContext and use PreferencesContext instead 2024-01-23 22:59:43 +08:00
Jon Eugster 36bc52c960 add logic game to landing page 2024-01-22 13:31:43 +01:00
ran ab98eaa3ba Change the selected button to a slider 2024-01-16 11:21:46 +08:00
ran d16956da9b Modify the props definition of the preference popup component 2024-01-12 23:43:21 +08:00
ran 8c93b3c5b3 Modify logic for all preferences 2024-01-12 23:29:03 +08:00
Alexander Bentkamp c9f97b3285 remove watchdog 2023-12-15 22:17:09 +01:00
Jon Eugster 5a78118bb6 improve display of buttons on mobile 2023-12-14 23:04:18 +01:00
Jon Eugster a6775d5495 move 'show more help'-button on mobile #143 2023-12-14 22:13:44 +01:00
Jon Eugster 03a370464b fix altTitle for backwards compatibility 2023-12-14 22:06:53 +01:00
Jon Eugster eaa214ec37 improve world tree on mobile #101 2023-12-14 21:59:47 +01:00
Jon Eugster d7f1f70d41 Merge pull request #168 from Wzixiao/mobile-option 
Mobile option (template)
 2023-12-14 21:53:08 +01:00
Jon Eugster 1ab50710f5 fix: update rules slider on erasing progress #157 2023-12-14 21:24:08 +01:00