From 78d25576b8a3be2dbd39a0cf6ec3c95d0fb505b1 Mon Sep 17 00:00:00 2001
From: ragnar <git@rmgk.de>
Date: Fri, 17 Nov 2023 18:20:22 +0100
Subject: [PATCH] =?UTF-8?q?don=E2=80=99t=20include=20non=20chache=20files?=
 =?UTF-8?q?=20in=20repo?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

in other words, make »git clean -fdx« safe
---
 .gitignore                         | 1 -
 Modules/Microbenchmarks/.gitignore | 4 ----
 2 files changed, 5 deletions(-)
 delete mode 100644 Modules/Microbenchmarks/.gitignore

diff --git a/.gitignore b/.gitignore
index aac4d7e87..5d4701eeb 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,7 +2,6 @@
 .bsp/
 .idea/
 .metals/
-Local/
 metals.sbt
 node_modules/
 package-lock.json
diff --git a/Modules/Microbenchmarks/.gitignore b/Modules/Microbenchmarks/.gitignore
deleted file mode 100644
index 2bca49c59..000000000
--- a/Modules/Microbenchmarks/.gitignore
+++ /dev/null
@@ -1,4 +0,0 @@
-resultArchive/
-resultStore/
-fig*
-link.pl