This works too

nomeata · nomeata · commit ec4613f06e7d · 2025-05-22T16:14:39.000+02:00
diff --git a/tests/lean/run/inliner_loop.lean b/tests/lean/run/inliner_loop.lean
@@ -1,4 +1,3 @@
-set_option linearNoConfusionType false
 unsafe inductive t
 | mk : (t → t) → t
 

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,3 @@`
`1`		`-set_option linearNoConfusionType false`
`2`	`1`	`unsafe inductive t`
`3`	`2`	`\| mk : (t → t) → t`
`4`	`3`