Bug#1008534: devhelp: No page open

2022-07-15 Thread Phil Armstrong
On Thu, 05 May 2022 09:47:07 -0700 Tor Slettnes wrote: Shouldn't this be a higher priority than "normal"? It basically makes "devhelp" unusable. As of today, 15th July 2022, this bug seems to be fixed, at least on my Debian testing desktop. There hasn’t been a devhelp release, so presumably

Bug#1008534: devhelp: No page open

2022-05-05 Thread Tor Slettnes
Shouldn't this be a higher priority than "normal"? It basically makes "devhelp" unusable.