tools: remove src/tools/codelines master github/master
authorBruce Momjian <bruce@momjian.us>
Sat, 22 Nov 2025 17:01:56 +0000 (12:01 -0500)
committerBruce Momjian <bruce@momjian.us>
Sat, 22 Nov 2025 17:02:14 +0000 (12:02 -0500)
commitc0bc9af15197e3604a6ec205a7485de21b0b21af
tree35ca02ad47c2c7d589ae1ec72b10322f900c0c3d
parent5eed8ce50ce9df1067b95593dde9f4fc526dfc72
tools:  remove src/tools/codelines

This is a one-line script never gained general usage since being added
in 2005.

Backpatch-through: master
src/tools/codelines [deleted file]