bug#66283: 30.0.50; which-function-mode: When configured to display in header, and toggling off, then does not remove header

[Mekeor Melire]

2023-10-04 11:13 sbaugh@janestreet.com:

> From 9918722015e52510b12b0eeee093f11e231d14fe Mon Sep 17 
> 00:00:00 2001
> From: Spencer Baugh <sbaugh@janestreet.com>
> Date: Wed, 4 Oct 2023 09:53:47 -0400
> Subject: [PATCH] Remove the header line after disabling 
> which-function-mode

Thank you! I tested this patch quickly and simply, and it works for me.

By the way, I'd also suggest to make which-function-mode not buffer-local 
instead of global. But I guess I should submit another bug-report for this.