/* Record the values of window-min-width and window-min-height
so that window sizes remain consistent with them. */
int min_width, min_height;
/* Record the values of window-min-width and window-min-height
so that window sizes remain consistent with them. */
int min_width, min_height;