Skip to content

Commit

Permalink
correct std version
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Nov 28, 2023
1 parent a57a5af commit dfb2f10
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 3 deletions.
4 changes: 2 additions & 2 deletions server/lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@
[{"url": "https://github.com/leanprover/std4.git",
"type": "git",
"subDir": null,
"rev": "bf8a6ea960d5a99f8e30cbf5597ab05cd233eadf",
"rev": "a652e09bd81bcb43ea132d64ecc16580b0c7fa50",
"name": "std",
"manifestFile": "lake-manifest.json",
"inputRev": null,
"inputRev": "v4.3.0-rc2",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "GameServer",
Expand Down
5 changes: 4 additions & 1 deletion server/lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,10 @@ open Lake DSL

package GameServer

require std from git "https://github.com/leanprover/std4.git"
-- Using this assumes that each dependency has a tag of the form `v4.X.0`.
def leanVersion : String := s!"v{Lean.versionString}"

require std from git "https://github.com/leanprover/std4.git" @ leanVersion

lean_lib GameServer

Expand Down

0 comments on commit dfb2f10

Please sign in to comment.