From 799bd29627c554f83c1ec9b4a226a739632cbc29 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 20 Nov 2019 15:31:57 +0100
Subject: Document -vos flag for coqdep

---
 tools/coqdep.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tools')

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index b9a8601d10..7a401160db 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -455,6 +455,7 @@ let usage () =
   eprintf "  -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *)
   eprintf "  -R dir logname : add and import dir recursively to coq load path under logical name logname\n";
   eprintf "  -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n";
+  eprintf "  -vos : also output dependencies about .vos files\n";
   eprintf "  -dumpgraph f : print a dot dependency graph in file 'f'\n";
   eprintf "  -dumpgraphbox f : print a dot dependency graph box in file 'f'\n";
   eprintf "  -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n";
-- 
cgit v1.2.3