49062cc3d5
add new game
3 weeks ago
1845644e86
Extract fetching of stats and perform it every 2 seconds
3 weeks ago
451dc262b2
Fixed display error of server capacity by performing rounding as last step.
1 month ago
52898d93e7
Fix turning stats to zero by casting them to int before multiplying.
2 months ago
ae38ad977a
update redirects
2 months ago
0e58e81875
parse CPU/MEM usage as integer.
3 months ago
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
3 months ago
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/
4 months ago
25141b9613
add some translation keys
4 months ago
6a8abf41bd
implement stats script
5 months ago
1466a41169
fix fetch url for stats
5 months ago
3cdb9a026b
fix stats
5 months ago
ebd7268421
feat: add option to display server capacity
5 months ago
5a404a9a58
Generate translation.json of Korean
5 months ago
cebea6a6aa
Add Korean on config.json
5 months ago
c20d807d5c
add default language configuration
7 months ago
6bd9e95db9
update zh-translation
8 months ago
6b5fc80896
Update client/public/locales/es/translation.json
9 months ago
e56c7a0670
Update client/public/locales/es/translation.json
9 months ago
5b710da197
Update client/public/locales/es/translation.json
9 months ago
b275bbb94f
Update translation.json
...
Spanish translation of the UI.
9 months ago
29eb90e6c8
add spanish
9 months ago
a523bab1d6
fix css warning
10 months ago
499bb00d4f
fix language loading on landing page
10 months ago
d456621875
apply suggestions from PR #206 manually
10 months ago
a8d3169ebb
add some translation keys
11 months ago
9b05a27888
use translation of level title
11 months ago
3124d90cd6
typo
11 months ago
5a768c25b7
mark two more translations
11 months ago
39be34e83a
improve landing page
11 months ago
684a1bc72b
fix initial translation loading on starting page
11 months ago
10391b616c
add chinese translations
11 months ago
aaa6c3b576
add german translations
11 months ago
d60dc3fcb2
mark most of the game text for translation
11 months ago
1a54edffd4
bump lean-i18n and other stuff
11 months ago
ad1add5264
support translations of the games
11 months ago
a26022e3fc
fix css
11 months ago
7c44d49b2a
images on all levels
11 months ago
a7784ef66b
center github icon
11 months ago
389e120117
add translations
11 months ago
ee9fd18a56
use global configs in i18n-scanner
11 months ago
8b29f88407
use flags for game tiles
11 months ago
ebda6cc162
more progress on internationalisation
11 months ago
7e9514fe96
mark all texts for translation #179
11 months ago
038dbe71b8
fix i18next-scanner overwriting existing translations
11 months ago
19d2ea363a
refactor i18next-scanner config
11 months ago
3ac8fdace7
mark translations in app-bar
11 months ago
8d0493acb5
make preferences work #179
11 months ago
b37f050da5
Merge pull request #204 from noamraph/patch-1
...
Update level.css - hide .katex-mathml, to fix scrolling issue
11 months ago
09c81ea43f
Update level.css - hide .katex-mathml, to fix scrolling issue
...
Fixes https://github.com/leanprover-community/lean4game/issues/202
11 months ago
Jon Eugster
matlorr
TentativeConvert
Bulhwi Cha
Taehyun Lee
rexwzh
miguelmarco
Noam Yorav-Raphael