Sorry. It's in the bug forum area. admin/doeditconfig.php and admin/doedittheme.php. All you have to do is rename the files. You can tell what they do from the name. If you're like me and you don't change your config often, you'll be fine just renameing them back and forth until they fix the bug. I only make config changes once a year or so.
