From 1207d5d018436e70a2ee386cb5644493c02cd983 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 29 Nov 2017 10:58:40 +0100
Subject: Documenting the possibility to pass filenames to coqchk.

---
 doc/refman/RefMan-com.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 8b1fc7c8f3..b4d9f60ebc 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -299,8 +299,9 @@ The following command-line options are recognized by the commands {\tt
 
 \section{Compiled libraries checker ({\tt coqchk})}
 
-The {\tt coqchk} command takes a list of library paths as argument.
-The corresponding compiled libraries (.vo files) are searched in the
+The {\tt coqchk} command takes a list of library paths as argument, described
+either by their logical name or by their physical filename, which must end in
+{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the
 path, recursively processing the libraries they depend on. The content
 of all these libraries is then type-checked. The effect of {\tt
   coqchk} is only to return with normal exit code in case of success,
-- 
cgit v1.2.3