void dispatch_ob(EventType e, int num0, int num1);
void dispatch_signal(int signal);
/* *x and *y should be set with the destination of the window, they may be
changed by the event handlers */
void dispatch_ob(EventType e, int num0, int num1);
void dispatch_signal(int signal);
/* *x and *y should be set with the destination of the window, they may be
changed by the event handlers */