Now handles extra (unspecified) options gracefully.
Authored by: keess 2006-08-31
Parent: [r1597]
Child: [r1599]