Fixes broken admin menu extension (#4351).
Authored by: jplang 2009-12-07
Parent: [r3130]
Child: [r3132]
