From e46e66e96017f6f8ca72624f86d9da6543739a5d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gr=C3=A9goire=20Paris?= <postmaster@greg0ire.fr>
Date: Mon, 22 Aug 2022 19:35:45 +0200
Subject: [PATCH] Remove remnants from Infection

Looks like it got lost when migrating to Github actions and removed from
composer.json during a merge up.

I think it would be hard to reintroduce it, and that that should not be
done on the next major branch in any case.
---
 .gitignore          |  1 -
 infection.json.dist | 14 --------------
 2 files changed, 15 deletions(-)
 delete mode 100644 infection.json.dist

diff --git a/.gitignore b/.gitignore
index 25afa3930..8f0a796ba 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,5 +3,4 @@
 /build
 /phpcs.xml
 /.phpcs-cache
-/infection.log
 /.phpunit.result.cache
diff --git a/infection.json.dist b/infection.json.dist
deleted file mode 100644
index da28db78e..000000000
--- a/infection.json.dist
+++ /dev/null
@@ -1,14 +0,0 @@
-{
-    "timeout": 2,
-    "source": {
-        "directories": [
-            "lib"
-        ]
-    },
-    "logs": {
-        "text": "infection.log"
-    },
-    "mutators": {
-        "@default": true
-    }
-}
\ No newline at end of file