Commit 2024-07-20 11:05 ef9d07a5

feat: add the refine linter, to flag uses of refine' (#11884) This PR introduces a linter to flag uses of refine', suggesting to use refine instead. refine and refine' are similar tactics, but they handle meta-variable slightly differently. This means that they are not completely interchangeable, but refine is more readable and (heuristically) tends to be more efficient on average. This linter is an incentive to discourage uses of refine', without being a ban. Zulip discussion.