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

Previous Next

Full log

View this message in rfc822 format

From: Eli Zaretskii <eliz <at> gnu.org>
To: Stefan Monnier <monnier <at> iro.umontreal.ca>
Cc: 70820 <at> debbugs.gnu.org, visuweshm <at> gmail.com
Subject: bug#70820: [PATCH] Editable grep buffers
Date: Sat, 18 May 2024 18:44:38 +0300

> From: Stefan Monnier <monnier <at> iro.umontreal.ca>
> Cc: Visuwesh <visuweshm <at> gmail.com>,  70820 <at> debbugs.gnu.org
> Date: Sat, 18 May 2024 09:35:58 -0400
> 
> > (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.

Yes, but how does compilation-mode know the other major-mode is
"unrelated"?  It could be very related, as this discussion
demonstrates.

Previous Next

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