diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index fcfd00cb40..613257c685 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -272,7 +272,8 @@ let all_target l = print "HTMLFILES=$(VFILES:.v=.html)\n"; print "GHTMLFILES=$(VFILES:.v=.g.html)\n"; print "\n"; - print "all: $(VOFILES)\n\n"; + print "all: "; print_list "\\\n " (fnames l); + print "\n\n"; if !some_vfile then begin print "spec: $(VIFILES)\n\n"; print "gallina: $(GFILES)\n\n"; |