All pages containing use of <source> and </source> tags, excluding User pages, have been modified to use <pre> and </pre> tags instead.
I did most of this by hand, and only later did I find the Replace_Text
extension for MediaWiki, which helped me find 2 others to fix up.
Anyway, because of the nature of all of this, I'm locking this thread. It would be nice if the syntax highlighter maintainers would actually maintain their software through official MediaWiki channels and so on, but it really doesn't look like that's going to happen. It was a good run, folks.