diff options
| author | Gaëtan Gilbert | 2019-11-20 15:31:57 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-21 14:31:12 +0100 |
| commit | 799bd29627c554f83c1ec9b4a226a739632cbc29 (patch) | |
| tree | 22d10310369f8be2488655785b04fd139bf22866 /man | |
| parent | b680b06b31c27751a7d551d95839aea38f7fbea1 (diff) | |
Document -vos flag for coqdep
Diffstat (limited to 'man')
| -rw-r--r-- | man/coqdep.1 | 3 |
1 files changed, 3 insertions, 0 deletions
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 |