From e525e2d3246c2540018f38e939ac784277ba1147 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 15 Apr 2015 11:01:19 +0200
Subject: Documenting the recommandation of toplevel-only commands.

---
 doc/refman/RefMan-oth.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 4952ed7785..7d7a4c9a0c 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -680,7 +680,8 @@ should use the command \texttt{Locate File} (see Section~\ref{Locate File})
 
 Loadpaths are preferably managed using {\Coq} command line options
 (see Section~\ref{loadpath}) but there remain vernacular commands to
-manage them.
+manage them for practical puposes. Such commands are only meant to be issued in
+the toplevel, and using them in source files is discouraged.
 
 \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
 This command displays the current working directory.
-- 
cgit v1.2.3