aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2001-09-19 15:53:19 +0000
committerfilliatr2001-09-19 15:53:19 +0000
commit00b1b8838d717f44cd2c309ab6db3f737ded801a (patch)
tree0ccff8931dfa1cfd301c2a3c0c875110cc261eca
parentb7194f41401f9f5ce1909b50a1c38e9b1f60b677 (diff)
la cible all était incomplète
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2003 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tools/coq_makefile.ml3
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";