diff --git a/examples/git/.gitignore b/examples/git/.gitignore new file mode 100644 index 0000000000..29035da63c --- /dev/null +++ b/examples/git/.gitignore @@ -0,0 +1,2 @@ +/build +/lean_packages diff --git a/examples/git/GitHello.lean b/examples/git/GitHello.lean new file mode 100644 index 0000000000..ccbbf4cfd0 --- /dev/null +++ b/examples/git/GitHello.lean @@ -0,0 +1 @@ +import Hello diff --git a/examples/git/clean.sh b/examples/git/clean.sh new file mode 100644 index 0000000000..ab33e94a34 --- /dev/null +++ b/examples/git/clean.sh @@ -0,0 +1,2 @@ +rm -rf build +rm -rf lean_packages diff --git a/examples/git/package.lean b/examples/git/package.lean new file mode 100644 index 0000000000..e4b312815c --- /dev/null +++ b/examples/git/package.lean @@ -0,0 +1,18 @@ +import Lake.Package + +open Lake System + +def package : PackageConfig := { + name := "gitHello" + version := "1.0" + dependencies := [ + { + name := "hello", + src := Source.git + "https://github.com/tydeu/lean4-lake.git" + "71defa066dd845a31d19547f1a3e01f79c5fc8d9" + (branch := none) + dir := FilePath.mk "examples" / "hello" + } + ] +} diff --git a/examples/git/package.sh b/examples/git/package.sh new file mode 100644 index 0000000000..b6449c2dd0 --- /dev/null +++ b/examples/git/package.sh @@ -0,0 +1 @@ +../../build/bin/Lake build-bin diff --git a/examples/git/test.sh b/examples/git/test.sh new file mode 100644 index 0000000000..17a6aca2f8 --- /dev/null +++ b/examples/git/test.sh @@ -0,0 +1,3 @@ +./clean.sh +./package.sh +./build/bin/gitHello diff --git a/examples/test.sh b/examples/test.sh index 84fa211f1f..1201d6ea1a 100644 --- a/examples/test.sh +++ b/examples/test.sh @@ -18,6 +18,11 @@ cd deps ./test.sh cd .. +echo 'testing git' +cd git +./test.sh +cd .. + echo 'testing ext' cd ext ./test.sh