You see, I should've known before I even opened my mouth-- this is Linux we're talking about; and if there's something worth doing, chances are that somebody created the tools to do it a long time ago.
ImageMagick is a fascinating set of tools, and it appears as though it will do exactly what I want (and near-infinitely more)-- if I can determine how to convert a bunch of files in one go. ImageMagick's 'convert' says it will convert an image or a sequence
of images, but figuring out the command syntax for the sequence business has been the tricky part. I haven't been able to find any clear documentation on it. Single-file format conversions, yes; batch jobs, no. I've read the man page, visited the official web site, Googled it, and so on with no clear answer.
Am I correct in guessing that it's reasonable that there sould be some kind of "wildcard" arrangement or similar, where I specify that I want all .jpg files in one directory to end up as .tif files in another, without having to enter filename after filename in the command line? I'm sorry if I'm missing something completely obvious, but I can't seem to figure it out.