[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 09:35:58 -0400 |
|
User-agent: |
Gnus/5.13 (Gnus v5.13) |
> (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
- 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 <=
- 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, 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