Subject: Re: bug#76084: 31.0.50; Dragging tab line does not resize windows, unlike header line or mode line

From: Jared Finder <[email-masked]>
Date: Sun, 13 Apr 2025 23:14:56 -0700

On 2025-02-28 01:25, martin rudalics wrote:
>> Thanks, I tried out your patch, and everything works nicely.
>> Looks like it's ready to be installed if Martin agrees?
> 
> I think it's ready.

Looks like installing the patch was forgotten.

The patch was attached to an earlier message in this thread. See 
https://debbugs.gnu.org/cgi/bugreport.cgi?bug=76084#23.

   -- MJF