aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar kirchner <kirchner@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-29 14:47:03 +0000
committerGravatar kirchner <kirchner@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-29 14:47:03 +0000
commit5b994899184a8837513094d7a185206b4831a353 (patch)
treee7c593253a395422586f2de48703368796857d55 /tools
parent4eaeba514ca5d2cfa42d57a1a8022c6337461356 (diff)
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5601 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml411
1 files changed, 10 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 66911531b..37013d02d 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -114,6 +114,10 @@ let standard sds =
printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name;
printf "\t$(COQBIN)coq_makefile -f %s -o %s\n" !make_name !makefile_name;
print "\n";
+ List.iter
+ (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n")
+ sds;
+ print "\n";
end;
print "clean:\n";
print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~\n";
@@ -127,6 +131,11 @@ let standard sds =
List.iter
(fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n")
sds;
+ print "\n";
+ print "html:\n";
+ List.iter
+ (fun x -> print "\t(cd "; print x; print " ; $(MAKE) html)\n")
+ sds;
print "\n"
let implicit () =
@@ -250,7 +259,7 @@ let subdirs l =
print ".PHONY: ";
print_list " "
("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install"
- :: "depend" :: "xml" :: sds);
+ :: "depend" :: "xml" :: "html" :: sds);
print "\n\n";
sds