phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,080 Commits 19 Branches 10 Tags
49062cc3d5c558b49ef1aae4d3132d011874b2bf
Commit Graph
465 Commits
Author SHA1 Message Date
Jon Eugster 49062cc3d5 add new game 2025-01-26 14:29:54 +01:00
matlorr 1845644e86 Extract fetching of stats and perform it every 2 seconds 2025-01-24 13:51:28 +01:00
matlorr 451dc262b2 Fixed display error of server capacity by performing rounding as last step. 2025-01-10 10:13:36 +01:00
matlorr 52898d93e7 Fix turning stats to zero by casting them to int before multiplying. 2024-12-28 11:13:11 +01:00
TentativeConvert ae38ad977a update redirects 2024-12-10 14:35:27 +01:00
Jon Eugster 0e58e81875 parse CPU/MEM usage as integer. 2024-11-25 12:38:16 +01:00
Marcus Zibrowius f0aa6b58ed Edits on landing page, with updates to German & Spanish translations. 
modified:   ../de/translation.json
	modified:   ../en/translation.json
	modified:   ../es/translation.json
	modified:   ../ko/target/translation.json
	modified:   translation.json
	modified:   ../../../src/components/landing_page.tsx
 2024-11-08 16:51:38 +01:00
Bulhwi Cha 64670d1579 fix config.json and add Korean translation 
* In the `config.json` file, the ISO code representing Korean should be
  `ko`, not `kr`.
* Remove the `client/public/locales/kr` subdirectory.
* Add the `client/public/locales/ko` subdirectory, which itself is the
  OmegaT project for the Korean translation of `lean4game`.

OmegaT[0] is a translation memory application intended for professional
translators. I use it to translate English documentation into Korean.

[0] https://omegat.org/
 2024-10-18 13:10:10 +09:00
Bulhwi Cha 25141b9613 add some translation keys 2024-10-17 20:03:46 +09:00
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
Taehyun Lee 5a404a9a58 Generate translation.json of Korean 2024-09-07 21:16:18 +09:00
Taehyun Lee cebea6a6aa Add Korean on config.json 2024-09-07 21:14:59 +09:00
rexwzh c20d807d5c add default language configuration 2024-07-11 01:51:17 +08:00
rexwzh 6bd9e95db9 update zh-translation 2024-06-23 13:53:19 +08:00
Jon Eugster 6b5fc80896 Update client/public/locales/es/translation.json 2024-06-02 10:34:18 +02:00
Jon Eugster e56c7a0670 Update client/public/locales/es/translation.json 2024-06-02 10:32:59 +02:00
Jon Eugster 5b710da197 Update client/public/locales/es/translation.json 2024-06-02 10:32:51 +02:00
miguelmarco b275bbb94f Update translation.json 
Spanish translation of the UI.
 2024-05-31 18:55:00 +02:00
Jon Eugster 29eb90e6c8 add spanish 2024-05-31 13:00:43 +02:00
Jon Eugster a523bab1d6 fix css warning 2024-04-10 14:45:17 +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 3124d90cd6 typo 2024-03-29 12:36:39 +01: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 10391b616c add chinese translations 2024-03-28 20:45:50 +01:00
Jon Eugster aaa6c3b576 add german translations 2024-03-27 02:17:46 +01:00
Jon Eugster d60dc3fcb2 mark most of the game text for translation 2024-03-27 02:03:05 +01:00
Jon Eugster 1a54edffd4 bump lean-i18n and other stuff 2024-03-27 01:37:58 +01:00
Jon Eugster ad1add5264 support translations of the games 2024-03-27 00:22:51 +01:00
Jon Eugster a26022e3fc fix css 2024-03-26 19:10:23 +01:00
Jon Eugster 7c44d49b2a images on all levels 2024-03-26 17:24:53 +01:00
Jon Eugster a7784ef66b center github icon 2024-03-26 10:04:39 +01:00
Jon Eugster 389e120117 add translations 2024-03-26 02:49:48 +01:00
Jon Eugster ee9fd18a56 use global configs in i18n-scanner 2024-03-26 01:16:21 +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 038dbe71b8 fix i18next-scanner overwriting existing translations 2024-03-25 23:00:05 +01:00
Jon Eugster 19d2ea363a refactor i18next-scanner config 2024-03-25 22:44:26 +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 b37f050da5 Merge pull request #204 from noamraph/patch-1 
Update level.css - hide .katex-mathml, to fix scrolling issue
 2024-03-25 18:51:48 +01:00
Noam Yorav-Raphael 09c81ea43f Update level.css - hide .katex-mathml, to fix scrolling issue 
Fixes https://github.com/leanprover-community/lean4game/issues/202
 2024-03-25 19:10:33 +02:00