Skip to content

Commit fdae48b

Browse files
committed
Depend on importGraph via reservoir, not git.
1 parent 9eedba6 commit fdae48b

File tree

2 files changed

+2
-3
lines changed

2 files changed

+2
-3
lines changed

spec/fixtures/example-project/lake-manifest.json

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@
3131
{"url": "https://github.com/leanprover-community/import-graph",
3232
"type": "git",
3333
"subDir": null,
34-
"scope": "",
34+
"scope": "leanprover-community",
3535
"rev": "ac7b989cbf99169509433124ae484318e953d201",
3636
"name": "importGraph",
3737
"manifestFile": "lake-manifest.json",

spec/fixtures/example-project/lakefile.toml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@ path = "foo"
77

88
[[require]]
99
name = "importGraph"
10-
git = "https://github.com/leanprover-community/import-graph"
11-
rev = "main"
10+
scope = "leanprover-community"
1211

1312
[[lean_lib]]
1413
name = "Test"

0 commit comments

Comments
 (0)