From b1a03b1b5a2117bb91be14009e91d198418220d6 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Mon, 13 Oct 2025 10:34:56 +0200
Subject: [PATCH] chore: delete unused test file

This file as added in #29513, but never hooked up to the unit tests.
It is thus unused; delete it.
---
 MathlibTest/LintStyle2.lean | 6 ------
 1 file changed, 6 deletions(-)
 delete mode 100644 MathlibTest/LintStyle2.lean

diff --git a/MathlibTest/LintStyle2.lean b/MathlibTest/LintStyle2.lean
deleted file mode 100644
index 70a8a5bbb38ab9..00000000000000
--- a/MathlibTest/LintStyle2.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-import MathlibTest.LintStyle
-
-/-! Test for calling lint-style with its default options: this file has intentional style
-lint errors. -/
-
-set_option profiler.threshold 50