diff --git a/ChangeLog b/ChangeLog
index 3abf8efb4..c34527616 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,7 +1,12 @@
 2005-01-29  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* bench/emptchk/README: Make clearer that spin is needed.
+
 	* src/tgbatest/randtgba.cc (syntax): Missing std::endl.
 
+2005-01-29  Alexandre Duret-Lutz  <adl@gnu.org>
+	    Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
+
 	* bench/Makefile.am, bench/emptchk/Makefile.am,
 	bench/emptchk/README, bench/emptchk/algorithms,
 	bench/emptchk/defs.in, bench/emptchk/ltl-human.sh,
diff --git a/bench/emptchk/README b/bench/emptchk/README
index 943ec870f..434c97bd3 100644
--- a/bench/emptchk/README
+++ b/bench/emptchk/README
@@ -144,8 +144,11 @@ This directory contains:
  USAGE
 =======
 
-  1. If that is not done already, configure and compile all Spot library,
-     then come back into this directory.
+  0. Install SPIN (spinroot.com), and make sure the `spin' binary is in
+     your path.
+
+  1. If that is not done already, configure and compile all the Spot
+     library, then come back into this directory.
 
   2. Run `make' in this directory.  This will call pml2tgba.pl to
      generate the TGBA input for the two pml-*.sh tests.