function setWindowSize() {
    window.resizeTo(1400,1024);
}

// Local variables:
// mode: ecmascript
// end: