diff --git a/ChangeLog b/ChangeLog
index 4a02bc62b..679def516 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,7 @@
+2011-08-17  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* src/tgbatest/ltl2tgba.cc (syntax): -N implies -DS, not -D.
+
 2011-07-26  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* iface/dve2/dve2check.cc: Add option -W and simplify formulae.
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 98ed72f38..2afffc858 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -265,10 +265,10 @@ syntax(char* prog)
 	    << "  -K    dump the graph of SCCs in dot format" << std::endl
 	    << "  -KV   verbosely dump the graph of SCCs in dot format"
 	    << std::endl
-	    << "  -N    output the never clain for Spin (implies -D)"
+	    << "  -N    output the never clain for Spin (implies -DS)"
 	    << std::endl
 	    << "  -NN   output the never clain for Spin, with commented states"
-	    << " (implies -D)" << std::endl
+	    << " (implies -DS)" << std::endl
 	    << "  -O    tell if a formula represents a safety, guarantee, "
 	    << "or obligation property"
 	    << std::endl