diff options
| author | Guillaume Melquiond | 2015-02-24 14:38:49 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-02-24 14:38:49 +0100 |
| commit | def8cafc0ceae48d57a44ae120730ea36cb56b88 (patch) | |
| tree | 9ec078a6983a42ec441652fcc2bfea9ab710c90f | |
| parent | 061519fe518fc090a727957f7e46cbe67e10c633 (diff) | |
Update the list of phony targets produced by coq_makefile. (Fix for bug #4084)
Also make uninstall_me.sh a real target with proper dependencies.
| -rw-r--r-- | tools/coq_makefile.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 5213d38e71..b84d15d62e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -297,7 +297,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in print "\tprintf 'cd \"$${DSTROOT}\"$(COQDOCINSTALL) && "; printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind in - print "uninstall_me.sh:\n"; + printf "uninstall_me.sh: %s\n" !makefile_name; print "\techo '#!/bin/sh' > $@ \n"; if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs; uninstall_by_root where_what_oth; @@ -701,9 +701,12 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = main_targets vfiles mlfiles other_targets inc; print ".PHONY: "; print_list " " - ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" :: - "uninstall_me.sh" :: "uninstall" :: "userinstall" :: "depend" :: - "html" :: "validate" :: + ("all" :: "archclean" :: "beautify" :: "byte" :: "clean" :: + "gallina" :: "gallinahtml" :: "html" :: + "install" :: "install-doc" :: "install-natdynlink" :: "install-toploop" :: + "opt" :: "printenv" :: "quick" :: + "uninstall" :: "userinstall" :: + "validate" :: "vio2vo" :: (sds@(CList.map_filter (fun (n,_,is_phony,_) -> if is_phony then Some n else None) sps))); |