Post date: Jan 18, 2018 12:55:59 PM
Better write this down before I need to look it up again.
To change a file from e.g. image-000000.png.txt to image-000000.txt, use
rename 's/.png.txt$/.txt/' *.txt
on the command line.