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.

Estimated changes