From 0b86c9a2b0fcf3a30717d4abf94efad011a7c692 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 8 Mar 2023 19:04:33 +0100 Subject: Add backends/lean/lakefile.lean --- backends/lean/.gitignore | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 backends/lean/.gitignore (limited to 'backends/lean/.gitignore') diff --git a/backends/lean/.gitignore b/backends/lean/.gitignore new file mode 100644 index 00000000..6aef0860 --- /dev/null +++ b/backends/lean/.gitignore @@ -0,0 +1,2 @@ +lake-packages/ +build/ \ No newline at end of file -- cgit v1.2.3