Jon Eugster
49062cc3d5
add new game
1 year ago
matlorr
1845644e86
Extract fetching of stats and perform it every 2 seconds
1 year ago
matlorr
451dc262b2
Fixed display error of server capacity by performing rounding as last step.
1 year ago
matlorr
52898d93e7
Fix turning stats to zero by casting them to int before multiplying.
1 year ago
TentativeConvert
ae38ad977a
update redirects
2 years ago
Jon Eugster
0e58e81875
parse CPU/MEM usage as integer.
2 years ago
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
2 years ago
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/
2 years ago
Jon Eugster
6a8abf41bd
implement stats script
2 years ago
Jon Eugster
1466a41169
fix fetch url for stats
2 years ago
Jon Eugster
3cdb9a026b
fix stats
2 years ago
Jon Eugster
ebd7268421
feat: add option to display server capacity
2 years ago
Taehyun Lee
cebea6a6aa
Add Korean on config.json
2 years ago
rexwzh
c20d807d5c
add default language configuration
2 years ago
Jon Eugster
29eb90e6c8
add spanish
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
Jon Eugster
038dbe71b8
fix i18next-scanner overwriting existing translations
2 years ago
Jon Eugster
3ac8fdace7
mark translations in app-bar
2 years ago
Jon Eugster
8d0493acb5
make preferences work #179
2 years ago
Jon Eugster
b37f050da5
Merge pull request #204 from noamraph/patch-1
...
Update level.css - hide .katex-mathml, to fix scrolling issue
2 years ago
Noam Yorav-Raphael
09c81ea43f
Update level.css - hide .katex-mathml, to fix scrolling issue
...
Fixes https://github.com/leanprover-community/lean4game/issues/202
2 years ago
Jon Eugster
ff12b34295
add suspense to wait for loading #179
2 years ago
Jon Eugster
45bc0468df
implement i18next and i18next-scanner
2 years ago
Jon Eugster
c24efb1377
Merge pull request #203 from JiechengZhao/main
...
add next_i18n
2 years ago
Jon Eugster
a9447a70d4
add interface buttons for i18n #179
2 years ago
Jon Eugster
ce9f5c7840
fix locked editor mode
2 years ago
Hydrogenbear
cb711205a2
Add react_i18n
2 years ago
Jon Eugster
f42829422d
delete hidden hints in chat on Retry
2 years ago
Jon Eugster
47297e4194
temporary fix to improve message on server crash
2 years ago
Jon Eugster
f3f077741d
fix client breaking if server timed out.
2 years ago