GNU bug report logs - #70820
[PATCH] Editable grep buffers

Previous Next

Full log

Message #68 received at 70820 <at> debbugs.gnu.org (full text, mbox):

From: Stefan Monnier <monnier <at> iro.umontreal.ca>
To: Eli Zaretskii <eliz <at> gnu.org>
Cc: 70820 <at> debbugs.gnu.org, Visuwesh <visuweshm <at> gmail.com>
Subject: Re: bug#70820: [PATCH] Editable grep buffers
Date: Sat, 18 May 2024 09:35:58 -0400

[Message part 1 (text/markdown, inline)]

> (I must admit that unconditionally removing the faces is not very
> friendly on the part of compilation-mode.  Stefan, are there better
> ways of doing that, perhaps?)

These are properties which the major mode (unconditionally) added, so it
doesn't seem unfriendly to remove them unconditionally when switching to
an unrelated major mode.


        Stefan

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.