feat: Initialize Korean document by using config.json

leanprover-community / lean4game

Server to host lean games.

https://adam.math.hhu.de

GNU General Public License v3.0

197 stars 35 forks source link

feat: Initialize Korean document by using config.json #259

Closed 0417taehyun closed 2 months ago

0417taehyun commented 2 months ago

What I've done

[x] Set configuration on config.json for document in Korean
[x] Initialize Korean document by using npm run translate

FYI

There are some people interested in Lean and build a community to contribute this game in Korean. We are going to contribute the details later hence I just created the structure of it through config.json.

joneugster commented 2 months ago

The diff only shows whitespace fixes. Did you maybe forget to include the changes you described in the description?

0417taehyun commented 2 months ago

@joneugster

Oh, I made a mistake. I close this and open the other one.

0417taehyun commented 2 months ago

@joneugster

Here is the right PR, #260