targets in Makefiles generated by coq_makefile

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4084
From: @fblanqui
Reported version: 8.4
CC: @fblanqui, @silene

[coqbot]

Comment author: @fblanqui

Hi!

A target 'depend' is declared .PHONY but is used nowhere. Shouldn't it be removed?

They are also existing targets that are not declared as .PHONY: printenv install-doc beautify spec gallina gallinahtml. Shouldn't these targets be declared in .PHONY too?

Now, shouldn't Chapter 15.3 of the Coq manual and the Makefiles generated by coq_makefile include some comments describing the possible targets and what they are for?

Frédéric.

[coqbot]

Comment author: @silene

Fixed by commit def8caf, including a few additional phony targets: quick, install-*, vio2vo.

I am not closing the bug yet since it is worth mentioning (some of) them in the documentation.

[Zimmi48]

I think targets were documented as part of the coq_makefile2 effort.