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