The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi.

You should use the following syntax instead:

coq_makefile -R my_lib_dir Lib


Le 14/05/2013 02:27, Gregory Malecha a écrit :
> Hello --
>
> Is there a way to get coq_makefile to notice the -as option that is 
> allowed after -I by
> coqc? For example:
>
> coqc -I my_library -as Lib ...
>
> works, but when I pass '-as Lib' to coq_makefile, it seems to 
> completely ignore it:
>
> coq_makefile -I my_library -as Lib ....
>
> will generate a Makefile that runs commands like
>
> coqc -I my_library ....
>
> If it isn't implemented yet, I might be able to write a patch if 
> someone can point me to the right place.
>
> Thank you.
>
> --
> gregory malecha
> http://www.people.fas.harvard.edu/~gmalecha/ 
> <http://www.people.fas.harvard.edu/%7Egmalecha/>