Commit 2024-03-14 16:09 c33c2724
View on Github →chore: remove tactics (#11365) More tactics that are not used, found using the linter at #11308. The PR consists of tactic removals, whitespace changes and replacing a porting note by an explanation.
chore: remove tactics (#11365) More tactics that are not used, found using the linter at #11308. The PR consists of tactic removals, whitespace changes and replacing a porting note by an explanation.