The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

The command bin/coq_makefile -impredicative-set > foo should returns the 
warning:
>> Please now use \"-arg -impredicative-set\" instead of 
>> \"-impredicative-set\" alone to be more uniform.
It does not. This is not my problem anymore :-)

Similarly, bin/coq_makefile -custom foo bar mli should have told you
>> Please now use \"-extra[-phony] result deps command\" instead of \"-custom 
>> command deps result\ ».
>> It follows makefile target declaration order and has a clearer semantic.
which would have answer your question.

Cheers,
Pierre B.

> Le 15 mars 2016 à 11:02, Matej Kosik 
> <5764c029b688c1c0d24a2e97cd764f AT gmail.com>
>  a écrit :
> 
> Hi,
> 
> I am now going over "Make" files which come with coq-contribs.
> 
> Some of them contain "-custom" commands.
> It does not seem to be documented, i.e.
> 
>       coq_makefile -h
> 
> does not mention it.
> 
> Is this undocumented (?) on purpose or by mistake?
> 
> Also, I would like to ask how is "-custom" command different from "-extra"
> (other than syntactically)
> 
> --
> 
> M