From 0a8d0181d4f9ae7440b0daf065511342cef41475 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 12 May 2018 13:53:10 +0200
Subject: Minor update of the documentation/man about the resource file.

---
 man/coqtop.1 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'man')

diff --git a/man/coqtop.1 b/man/coqtop.1
index b1fbb3262..084adfe45 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -110,7 +110,7 @@ print Coq version and exit
 
 .TP
 .B \-q
-skip loading of rcfile
+skip loading of rcfile (resource file) if any
 
 .TP
 .BI \-init\-file \ filename
-- 
cgit v1.2.3