max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: make git example clone local repo

Browse source
This commit is contained in:
tydeu 2022-06-10 15:25:34 -04:00
parent 144fbaf642
commit e6e2c2ab72
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/git/lakefile.lean
View file

@ -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 {