0.12dev: Merged [8243] from 0.11-stable (#8290 - Bugfix and cleanup of how config handles Option from registry).
Authored by: osimons 2009-05-26
Parent: [r8243]
Child: [r8245]