My server didn't like the names of the buttons with plus-
marks like (1+day.png) or parentheses ( (diff).png ). I
substituted underscores and uploaded them, but of course
couldn't change the names back, either. Where do I change
the code to access the images with the changed names, lib/
Theme.php, themes/MacOSX/themeinfo.php, or ...