From 9065ce55a89a3183d3fbdf07de09a1b1d1e295eb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 27 Jan 2020 11:15:03 +0100 Subject: [PATCH] chore: ignore test output files --- tests/lean/.gitignore | 1 + tests/lean/run/.gitignore | 4 ++++ 2 files changed, 5 insertions(+) create mode 100644 tests/lean/.gitignore create mode 100644 tests/lean/run/.gitignore diff --git a/tests/lean/.gitignore b/tests/lean/.gitignore new file mode 100644 index 0000000000..3bb636aca3 --- /dev/null +++ b/tests/lean/.gitignore @@ -0,0 +1 @@ +/readonly.txt \ No newline at end of file diff --git a/tests/lean/run/.gitignore b/tests/lean/run/.gitignore new file mode 100644 index 0000000000..ef22906aaf --- /dev/null +++ b/tests/lean/run/.gitignore @@ -0,0 +1,4 @@ +/foo.txt +/foo2.txt +/print_error.lean.cpp +/print_error.lean.out