From e6e2c2ab72ab5f51f3ee2ab2b0c461f80dffa530 Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 10 Jun 2022 15:25:34 -0400 Subject: [PATCH] test: make `git` example clone local repo --- examples/git/lakefile.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/git/lakefile.lean b/examples/git/lakefile.lean index 1674e9f983..f5518efa82 100644 --- a/examples/git/lakefile.lean +++ b/examples/git/lakefile.lean @@ -4,8 +4,8 @@ open System Lake DSL package git_hello -require hello from git - "https://github.com/leanprover/lake.git"@"master"/"examples"/"hello" +require hello from + git "../.."@"master"/"examples"/"hello" @[defaultTarget] lean_exe git_hello {