[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#70820: [PATCH] Editable grep buffers
From: |
Visuwesh |
Subject: |
bug#70820: [PATCH] Editable grep buffers |
Date: |
Mon, 20 May 2024 15:40:47 +0530 |
User-agent: |
Gnus/5.13 (Gnus v5.13) |
[சனி மே 18, 2024] Eli Zaretskii wrote:
>> From: Stefan Monnier <monnier@iro.umontreal.ca>
>> Cc: visuweshm@gmail.com, 70820@debbugs.gnu.org
>> Date: Sat, 18 May 2024 12:27:06 -0400
>>
>> >> 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.
>>
>> If it's related it has access to internals, so it can so things like
>> disabling `compilation--remoave-properties`.
>
> OK, so my suggestion to Visuwesh is the best way of dealing with this.
> Fine by me.
Thank you Stefan & Eli, I will take a closer look at your suggestions
when time permits. I have limited internet access outside my work hours
so I cannot reply to your messages in full.
- bug#70820: [PATCH] Editable grep buffers, (continued)
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/08
- bug#70820: [PATCH] Editable grep buffers, Visuwesh, 2024/05/08
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/08
- bug#70820: [PATCH] Editable grep buffers, Visuwesh, 2024/05/09
- bug#70820: [PATCH] Editable grep buffers, Visuwesh, 2024/05/12
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/18
- bug#70820: [PATCH] Editable grep buffers, Stefan Monnier, 2024/05/18
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/18
- bug#70820: [PATCH] Editable grep buffers, Stefan Monnier, 2024/05/18
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/18
- bug#70820: [PATCH] Editable grep buffers,
Visuwesh <=
- bug#70820: [PATCH] Editable grep buffers, Stefan Monnier, 2024/05/18
- bug#70820: [PATCH] Editable grep buffers, Jim Porter, 2024/05/08
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/08
- bug#70820: [PATCH] Editable grep buffers, Jim Porter, 2024/05/08
- bug#70820: [PATCH] Editable grep buffers, Jim Porter, 2024/05/08
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/09
- bug#70820: [PATCH] Editable grep buffers, Jim Porter, 2024/05/09