This will prompt for new width and height of the graphics window (in pixels). Of course, the window may be resized in the usual way using the features of the window manager on your desktop. However, sometimes you might want to define an exact size, e.g. to make a series of snapshots, or mpeg_encode needs a multiple of 8 or 16 pixels. |

