From 82efa61f6c463ef5e0ad80e8b9db5b70b3c236d5 Mon Sep 17 00:00:00 2001 From: Chris Kipp Date: Wed, 7 Jun 2023 09:41:54 +0200 Subject: [PATCH] chore: remove unused semanticdb directory From looking back it seems that what this directory used to contain was removed in https://github.com/lampepfl/dotty/commit/bd2f8a6a30f8c03d988aaf100f2dcb8e7986848e, however the directory still remained. This PR just removes the leftover `build.properties`, which keeps getting updated, but does nothing. [Cherry-picked 0a9ebddaef4f3287b18e3ffc7c170f4d2649e2bd] --- semanticdb/project/build.properties | 1 - 1 file changed, 1 deletion(-) delete mode 100644 semanticdb/project/build.properties diff --git a/semanticdb/project/build.properties b/semanticdb/project/build.properties deleted file mode 100644 index 46e43a97ed86..000000000000 --- a/semanticdb/project/build.properties +++ /dev/null @@ -1 +0,0 @@ -sbt.version=1.8.2