Nicholas Nethercote cac0a0742b Remove the box_pointers lint.
As the comment says, this lint "is mostly historical, and not
particularly useful". It's not worth keeping it around.
2024-06-27 08:55:28 +10:00
..
2024-06-27 08:55:28 +10:00
2024-04-16 17:17:46 +01:00