From 8c0f9b63cb923a6cb6682124cd48db5da391075c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 24 Jan 2014 14:37:45 +0100
Subject: -schedule-vi-checking ported to spawn

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

(limited to 'doc/refman/AsyncProofs.tex')

diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 86bec7c21..3dcd762aa 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -124,8 +124,9 @@ The $coqtop -schedule-vi-checking 3 a b c$ command can be used to obtain
 a good scheduling for 3 workers to check all proof tasks of $a.vi$, $b.vi$ and
 $c.vi$.  Auxiliary files are used to predict how long a proof task will take,
 assuming it will take the same amount of time it took last time.
-The output of $coqtop -schedule-vi-checking$ is a list of commands one has
-to execute in order to check all proof tasks.
+If the $Makefile$ one uses was produced by $coq\_makefile$ the $checkproofs$
+target can be used to check all $.vi$ files.  The variable $J$ should be
+set to the number of workers, like in $make checkproofs J=3$.
 
 \subsubsection{Caveats}
 
-- 
cgit v1.2.3

