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

---
 man/coqdep.1 | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'man')

diff --git a/man/coqdep.1 b/man/coqdep.1
index 4639a75677..02c9d4390c 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -104,6 +104,9 @@ Skips subdirectory
 .TP 
 .B \-sort
 Output the given file name ordered by dependencies.
+.TP
+.B \-vos
+Output dependencies for .vos files (this is not the default as it breaks dune's Coq mode)
 .TP 
 .B \-boot
 For coq developers, prints dependencies over coq library files
-- 
cgit v1.2.3