[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#70820: [PATCH] Editable grep buffers
From: |
Stefan Monnier |
Subject: |
bug#70820: [PATCH] Editable grep buffers |
Date: |
Sat, 18 May 2024 12:27:06 -0400 |
User-agent: |
Gnus/5.13 (Gnus v5.13) |
>> 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`.
Stefan
- bug#70820: [PATCH] Editable grep buffers, (continued)
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/07
- bug#70820: [PATCH] Editable grep buffers, Visuwesh, 2024/05/07
- 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 <=
- bug#70820: [PATCH] Editable grep buffers, Eli Zaretskii, 2024/05/18
- bug#70820: [PATCH] Editable grep buffers, Visuwesh, 2024/05/20
- 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