From def8cafc0ceae48d57a44ae120730ea36cb56b88 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 24 Feb 2015 14:38:49 +0100
Subject: 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.
---
 tools/coq_makefile.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'tools')

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)));
-- 
cgit v1.2.3


From f712a0523359d5b54b4d4160bc77271fdde094a3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 14:33:07 +0100
Subject: Mention -R option in warnings, fixing #4067 and #4068.

---
 tools/coq_makefile.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b84d15d62e..bd78fe2c54 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -48,7 +48,8 @@ let usage () =
 
 coq_makefile [subdirectory] .... [file.v] ... [file.ml[i4]?] ...
   [file.ml{lib,pack}] ... [-extra[-phony] result dependencies command]
-  ... [-I dir] ... [-R physicalpath logicalpath] ... [VARIABLE = value]
+  ... [-I dir] ... [-R physicalpath logicalpath]
+  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]
   ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
   [-h] [--help]
 
@@ -767,10 +768,10 @@ let check_overlapping_include (_,inc_i,inc_r) =
     | [] -> ()
     | (pdir,_,abspdir)::l ->
 	if not (is_prefix pwd abspdir) then
-	  Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir;
+	  Printf.eprintf "Warning: in option -R/-Q, %s is not a subdirectory of the current directory\n" pdir;
 	List.iter (fun (pdir',_,abspdir') ->
 	  if is_prefix abspdir abspdir' || is_prefix abspdir' abspdir then
-	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
+	    Printf.eprintf "Warning: in options -R/-Q, %s and %s overlap\n" pdir pdir') l;
   in aux (inc_i@inc_r)
 
 let do_makefile args =
-- 
cgit v1.2.3


From b4a16a43d9f84969feb7b8b090092260cb898e23 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 15:03:36 +0100
Subject: Fixing printing error in coq_makefile.

---
 tools/coq_makefile.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index bd78fe2c54..84b4b5e5df 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -158,7 +158,7 @@ let vars_to_put_by_root var_x_files_l (inc_ml,inc_i,inc_r) =
   |l ->
     try
       let out = List.assoc "." (List.rev_map (fun (p,l,_) -> (p,l)) l) in
-      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option" in
+      let () = prerr_string "Warning: install rule assumes that -R/-Q . _ is the only -R/-Q option\n" in
       (None,[".",physical_dir_of_logical_dir out,List.rev_map fst var_x_files_l])
     with Not_found ->
       (
-- 
cgit v1.2.3