DESIRED_HEADER_LINE_HEIGHT 20571 src/xdisp.c    	  && CURRENT_HEADER_LINE_HEIGHT (w) != DESIRED_HEADER_LINE_HEIGHT (w))
DESIRED_HEADER_LINE_HEIGHT 20576 src/xdisp.c    	    = DESIRED_HEADER_LINE_HEIGHT (w);