Skip to content

Commit

Permalink
drop importGraph dependency in server
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Feb 14, 2024
1 parent c0acde1 commit 800d1f3
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 19 deletions.
18 changes: 0 additions & 18 deletions server/lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -9,24 +9,6 @@
"manifestFile": "lake-manifest.json",
"inputRev": "v4.5.0",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/import-graph",
"type": "git",
"subDir": null,
"rev": "a6b484980b41aab874fb3113ec5245bd91b625d8",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.4.0",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "GameServer",
"lakeDir": ".lake"}
2 changes: 1 addition & 1 deletion server/lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ def leanVersion : String := s!"v{Lean.versionString}"

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

require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
-- require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion

lean_lib GameServer

Expand Down

0 comments on commit 800d1f3

Please sign in to comment.