fix gameserver version
This commit is contained in:
@@ -28,9 +28,9 @@
|
|||||||
{"git":
|
{"git":
|
||||||
{"url": "https://github.com/leanprover-community/lean4game.git",
|
{"url": "https://github.com/leanprover-community/lean4game.git",
|
||||||
"subDir?": "server",
|
"subDir?": "server",
|
||||||
"rev": "52b42544ac8bcdbf4655e9c3a99567d924bd0caf",
|
"rev": "f5eb185eb22d6ff3ade9639a2c818a0dc6abc930",
|
||||||
"name": "GameServer",
|
"name": "GameServer",
|
||||||
"inputRev?": "main"}},
|
"inputRev?": "f5eb185eb22d6ff3ade9639a2c818a0dc6abc930"}},
|
||||||
{"git":
|
{"git":
|
||||||
{"url": "https://github.com/leanprover/std4",
|
{"url": "https://github.com/leanprover/std4",
|
||||||
"subDir?": null,
|
"subDir?": null,
|
||||||
|
|||||||
@@ -8,7 +8,7 @@ def LocalGameServer : Dependency := {
|
|||||||
|
|
||||||
def RemoteGameServer : Dependency := {
|
def RemoteGameServer : Dependency := {
|
||||||
name := `GameServer
|
name := `GameServer
|
||||||
src := Source.git "https://github.com/leanprover-community/lean4game.git" "main" "server"
|
src := Source.git "https://github.com/leanprover-community/lean4game.git" "f5eb185eb22d6ff3ade9639a2c818a0dc6abc930" "server"
|
||||||
}
|
}
|
||||||
|
|
||||||
/- Choose dependency depending on the environment variable NODE_ENV -/
|
/- Choose dependency depending on the environment variable NODE_ENV -/
|
||||||
|
|||||||
Reference in New Issue
Block a user