Commit Graph

1073 Commits (686b3b62616871e025fba0c690547dbd04f8ce6e)
 

Author SHA1 Message Date
Bulhwi Cha 686b3b6261 update translated segments in OmegaT project
There are slight changes only in some segments in the OmegaT project for
the Korean translation of `lean4game`. The actual Korean translation
remains the same.
1 year ago
Bulhwi Cha dd6a1380a1 correct mistranslation of names 1 year ago
matlorr 52898d93e7 Fix turning stats to zero by casting them to int before multiplying. 1 year ago
matlorr 5f30572741 Merge branch 'main' of github.com:leanprover-community/lean4game 1 year ago
matlorr 76f2414bd5 Refactor stats.sh to be more efficient. 1 year ago
Jon Eugster f1f9325c54 update gitignore 1 year ago
matlorr bd3375ada7 Create CPU-usage script 1 year ago
ADAM 64f34acd7a TMP: set github token 2 years ago
TentativeConvert ae38ad977a
update redirects 2 years ago
TentativeConvert a191c47b8e
update queue of pre-loaded games 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
Matvey Lorkish 045b1ea3fb
Merge pull request #261 from leanprover-community/stats
feat: improved stat logging
2 years ago
matlorr dc6f7b2822 Specify that logs should be created relative to the current working directory. 2 years ago
Jon Eugster db5ac7ed15
Merge pull request #269 from chabulhwi/fix-korean
fix `config.json` and add Korean translation
2 years ago
Jon Eugster 6a0e739301
Merge pull request #267 from chabulhwi/update-npm-deps
update npm deps
2 years ago
Jon Eugster ed96cf9534
Merge pull request #268 from chabulhwi/add-translation-keys
add some translation keys
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
Bulhwi Cha 25141b9613 add some translation keys 2 years ago
Bulhwi Cha ab9d0d0679 add some translation keys 2 years ago
Bulhwi Cha 6dca770dbf update npm deps 2 years ago
matlorr 2022fa9a44 Added logging game-access data 2 years ago
Jon Eugster b77afebe0a add sample 2 years ago
matlorr 4ac38ef7dd Refactored stats.sh to display approx. cpu usage and mem usage in .csv format 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
Jon Eugster af15982804
Merge pull request #260 from 0417taehyun/feat/generate-structure-of-korean-document
feat: Generate a structure of Korean document
2 years ago
Taehyun Lee 5a404a9a58 Generate translation.json of Korean 2 years ago
Taehyun Lee cebea6a6aa Add Korean on config.json 2 years ago
Jon Eugster 36499c0257 add note for servers with different base url 2 years ago
Jon Eugster 8c5e47dd7b improve doc, adaptation of #250
Co-authored-by: JadAbouHawili <jad-abou-hawili@hotmail.com>
2 years ago
Jon Eugster a46840d327
Merge pull request #253 from pitmonticone/fix-typos
Fix typos
2 years ago
Pietro Monticone f518efc81c Update LetIntros.lean 2 years ago
Pietro Monticone 9b93e3817d Update RpcHandlers.lean 2 years ago
Pietro Monticone 54c1e0dcaf Update FileWorker.lean 2 years ago
Pietro Monticone 2c1e69611b Update Commands.lean 2 years ago
Pietro Monticone 2c22c445b1 Update AbstractCtx.lean 2 years ago
Pietro Monticone b6b31a06ac Update README.md 2 years ago
Jon Eugster 255839fea7
Merge pull request #248 from Lean-zh/main
Environment Variable for Default Language Setting
2 years ago
Jon Eugster b961030db2
Update hints.md 2 years ago
rexwzh c20d807d5c add default language configuration 2 years ago
Jon Eugster 23c8099401
Merge pull request #244 from RexWzh/main
Update ZH-Translation for Lean Game Server
2 years ago
rexwzh 6bd9e95db9 update zh-translation 2 years ago
Jon Eugster 1febc51791
Update create_game.md 2 years ago
Jon Eugster d53b57a764
Update create_game.md 2 years ago
Jon Eugster 020b4f7803
Update create_game.md 2 years ago
Jon Eugster 0ae099414c
Update create_game.md 2 years ago
Jon Eugster b091ec579b
Merge pull request #236 from RexWzh/main
Fix Bug with Environment Variables for Ports
2 years ago