From aef4a7159b38b4ba9a5531b2fd97cc06bf90895c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 25 Jul 2019 12:52:38 +0200 Subject: [PATCH] chore(*): remove obsolete leanpkg.path files --- doc/examples/compiler/leanpkg.path | 2 -- library/leanpkg.path | 1 - tests/bench/leanpkg.path | 2 -- tests/lean/leanpkg.path | 2 -- tests/playground/leanpkg.path | 2 -- tests/playground/parser/leanpkg.path | 2 -- 6 files changed, 11 deletions(-) delete mode 100644 doc/examples/compiler/leanpkg.path delete mode 100644 library/leanpkg.path delete mode 100644 tests/bench/leanpkg.path delete mode 100644 tests/lean/leanpkg.path delete mode 100644 tests/playground/leanpkg.path delete mode 100644 tests/playground/parser/leanpkg.path diff --git a/doc/examples/compiler/leanpkg.path b/doc/examples/compiler/leanpkg.path deleted file mode 100644 index 2cbfd2b51b..0000000000 --- a/doc/examples/compiler/leanpkg.path +++ /dev/null @@ -1,2 +0,0 @@ -builtin_path -path . diff --git a/library/leanpkg.path b/library/leanpkg.path deleted file mode 100644 index c0926e3e67..0000000000 --- a/library/leanpkg.path +++ /dev/null @@ -1 +0,0 @@ -path . diff --git a/tests/bench/leanpkg.path b/tests/bench/leanpkg.path deleted file mode 100644 index a46b9ab3fb..0000000000 --- a/tests/bench/leanpkg.path +++ /dev/null @@ -1,2 +0,0 @@ -builtin_path -path . \ No newline at end of file diff --git a/tests/lean/leanpkg.path b/tests/lean/leanpkg.path deleted file mode 100644 index 2cbfd2b51b..0000000000 --- a/tests/lean/leanpkg.path +++ /dev/null @@ -1,2 +0,0 @@ -builtin_path -path . diff --git a/tests/playground/leanpkg.path b/tests/playground/leanpkg.path deleted file mode 100644 index a46b9ab3fb..0000000000 --- a/tests/playground/leanpkg.path +++ /dev/null @@ -1,2 +0,0 @@ -builtin_path -path . \ No newline at end of file diff --git a/tests/playground/parser/leanpkg.path b/tests/playground/parser/leanpkg.path deleted file mode 100644 index a46b9ab3fb..0000000000 --- a/tests/playground/parser/leanpkg.path +++ /dev/null @@ -1,2 +0,0 @@ -builtin_path -path . \ No newline at end of file