From 0ca2fe2e616f303665003bc6cf2d89df385f9394 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 23 May 2017 12:08:14 +0200
Subject: add the only target

This makes the following work correctly:
  make only TGTS="foo bar" -j2
note that
  make foo bar -j2
is not doing what you think
---
 doc/refman/RefMan-uti.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 104d7cd9e5..08cdbee503 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -132,6 +132,14 @@ as in {\tt make -f Makefile target} from another Makefile.
 	{\tt CoqMakefile.local}
 \end{itemize}
 
+\paragraph{Note: building a subset of the targets with -j}
+
+To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo}
+in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}.
+
+Note that \texttt{make foo.vo bar.vo -j} has a different meaning for
+the make utility, in particular it may build a shared prerequisite twice.
+
 \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
   \ttindex{coqdep}}
 
-- 
cgit v1.2.3