martin rudalics wrote:
> Can you try getting the results of `window--dump-frame' for these old
> (good and bad) configurations, that is with the build you used in your
> initial report?  I'd want to see different pixel heights (not 669) for
> these two frames but can't tell anything unless the pixel height (612)
> of the good window reemerges.
> 
> So try first to get the different (window-pixel-height) values back and
> then evaluate (window--dump-frame) instead of (window-pixel-height).

Trying to get the offending value back I figured out that the window
manager resizes the frame by one pixel when I move the frame from the
left side to the right one.  So, my original report was based on a
spurious intervention of the window manager.  Not moving the frame and
evaluating '(window-pixel-height)' results in the expected value of 613
for the *good* frame.  Sorry for the erroneous report.

-- 
 ,= ,-_-. =.  Bruno Félix Rezende Ribeiro (oitofelix) [0x28D618AF]
((_/)o o(\_)) There is no system but GNU;
 `-'(. .)`-'  GNU Linux-Libre is one of its official kernels;
     \_/      All software must be free as in freedom;