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