Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Commit 4eeaf3b

Browse files
committed
test: make git example clone local repo
1 parent 4d90870 commit 4eeaf3b

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Diff for: examples/git/lakefile.lean

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ open System Lake DSL
44

55
package git_hello
66

7-
require hello from git
8-
"https://github.com/leanprover/lake.git"@"master"/"examples"/"hello"
7+
require hello from
8+
git "../.."@"master"/"examples"/"hello"
99

1010
@[defaultTarget]
1111
lean_exe git_hello {

0 commit comments

Comments
 (0)