From 4db56fe2c963a4052f8415b3985c8765407fccbc Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 7 Mar 2023 17:49:03 +0100 Subject: Update the extraction of Lean files --- tests/lean/.gitignore | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 tests/lean/.gitignore (limited to 'tests/lean/.gitignore') diff --git a/tests/lean/.gitignore b/tests/lean/.gitignore new file mode 100644 index 00000000..e74f9899 --- /dev/null +++ b/tests/lean/.gitignore @@ -0,0 +1,2 @@ +*/lake-packages/ +*/build/ \ No newline at end of file -- cgit v1.2.3