The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

I tried another way:

putting the option --glob-from htmllinks for coqdoc in the makefile

then doing make html

as a result, each subdirectory has is proper index.html and html file 
for ecah module, but
none links within or between html files.

Is coqdoc truely compatible with multi-directories developments with a 
single makefile ?

Pierre


Pierre Casteran wrote:

> Hi.
>
> Which is the good option for coqdoc in case of a multi-directory 
> development ?
>
> I have a development splitted in various subdirectories D1 D2 D3.
>
> I call coq_makefile D1/*.v D2/*.v D3/*.v -I D1 -I D2 -I D3
> and I manage to have : COQC=$(COQBIN)coqc -dump-glob htmllinks
> and a target
>
> doc: $(VFILES)
>    $(COQDOC) --glob-from htmllinks \
>   $(VFILES)
>
>
> The problem is that all html files are put in the current directory 
> with names like
> D1.M1.html, D2.M2.html,  though the a- links in html files have the 
> (correct)
> form ".../D1/M1.html"
>
>
> Is there something to change in the call to coq_makefile and/or the 
> options to coqc and coqdoc ?
>
> Thanks,
> Pierre
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club