* (bug 7526) Make $wgDefaultUserOptions work again