From 2a703ebef927b1eaab43279efef4dde8c99c6384 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Aug 2020 15:41:10 +0200
Subject: Documentation of coq_makefile: fix name of installation dir + help on
 option -f.

---
 doc/sphinx/practical-tools/utilities.rst | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index d9992029ba..daae46ad11 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -89,10 +89,11 @@ invoking ``coq_makefile`` is the following one:
 Such command generates the following files:
 
 CoqMakefile
-  is a generic makefile for ``GNU Make`` that provides
-  targets to build the project (both ``.v`` and ``.ml*`` files), to install it
-  system-wide in the ``coq-contrib`` directory (i.e. where |Coq| is installed)
-  as well as to invoke coqdoc to generate HTML documentation.
+  is a makefile for ``GNU Make`` with targets to build the project
+  (e.g. generate .vo or .html files from .v or compile .ml* files)
+  and install it in the ``user-contrib`` directory where the |Coq|
+  library is installed. Run ``make`` with the ``-f CoqMakefile``
+  option to use ``CoqMakefile``.
 
 CoqMakefile.conf
   contains make variables assignments that reflect
-- 
cgit v1.2.3