function DUMMY() {
    // This does nothing but work around a Safari problem
}