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
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
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
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
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
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
Jon Eugster
ff12b34295
add suspense to wait for loading #179
2024-03-25 13:43:01 +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
1796c76a84
remove debugging css
2024-02-29 01:27:26 +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
Bulhwi Cha
Jon Eugster
Taehyun Lee
rexwzh
Noam Yorav-Raphael
Hydrogenbear