Paul Eggert Fri, 14 Jun 2024 20:58:24 -0700
On 2024-06-14 15:45, Bruno Haible wrote:
I propose to remove '.cppi-disable'.
Sounds good to me. I don't use cppi.