Subject: Re: [bug#73298] [PATCH 0/2] gnu: coq-mathcomp-bigenough: Use native-inputs.

From: Ludovic Courtès <[email-masked]>
Date: Sun, 17 Nov 2024 23:02:38 +0100

Hi,

Jean-Pierre De Jesus DIAZ <[email-masked]> skribis:

> This simplifies the coq-mathcomp-bigenough package by removing uneeded
> make flags and also moves coq and which from propagated-inputs to
> native-inputs.
>
> Jean-Pierre De Jesus DIAZ (2):
>   gnu: coq-mathcomp-bigenough: Use new style.
>   gnu: coq-mathcomp-bigenough: Use native-inputs.

I went ahead and applied both, even though I’m not on the Coq/OCaml
team.

I think you should consider joining that team (Julien, pukkamustard,
perhaps you could use some help?) and probably applying for commit
rights as well.

Thanks,
Ludo’.