diff --git a/bin/man/README b/bin/man/README
new file mode 100644
index 000000000..711b5ca8a
--- /dev/null
+++ b/bin/man/README
@@ -0,0 +1,14 @@
+To help with keeping man pages in sync with the binaries, the man page
+for PROGRAM is automatically generated from two sources:
+  1. the --help output of bin/PROGRAM,
+  2. the bin/man/PROGRAM.x file
+
+The tool help2man is responsible for doing this conversion.
+
+The PROGRAM.x file has [sections] headers to indicate sections.  The
+rest of the file uses groff macros for man pages.  For detail on this
+syntax, run "man groff_man".
+
+Note that some of the standard sections will be forced to the top or
+bottom of the manpage by help2man, the rest will appear as ordered in
+PROGRAM.x.
diff --git a/bin/man/dstar2tgba.x b/bin/man/dstar2tgba.x
index bb0b2e384..e5318bc0e 100644
--- a/bin/man/dstar2tgba.x
+++ b/bin/man/dstar2tgba.x
@@ -60,9 +60,13 @@ would make more sense.
 [BIBLIOGRAPHY]
 .TP
 1.
-<http://www.ltl2dstar.de/docs/ltl2dstar.html>
+.UR http://www.ltl2dstar.de/docs/ltl2dstar.html
+The
+.BR ltl2dstar manual
+.UE .
 
-Documents the output format of ltl2dstar.
+Documents the output format of
+.BR ltl2dstar .
 
 .TP
 2.
diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x
index e6c534cec..d0e6e94ab 100644
--- a/bin/man/spot-x.x
+++ b/bin/man/spot-x.x
@@ -55,17 +55,15 @@ convenient when chaining tools in a pipe.  Set this variable to
 passed to the printer by suffixing the output format with
 \fB=\fR and the options.  For instance running
 .in +4n
-.nf
-.ft C
+.EX
 % SPOT_DEFAULT_FORMAT=dot=bar autfilt ...
-.fi
+.EN
 .in -4n
 is the same as running
 .in +4n
-.nf
-.ft C
+.EX
 % autfilt --dot=bar ...
-.fi
+.EE
 .in -4n
 but the use of the environment variable makes more sense if you set
 it up once for many commands.
@@ -105,6 +103,7 @@ Specifies the default algorithm that should be used
 by the \f(CWis_obligation()\fR function.  The value should
 be one of the following:
 .RS
+.RS
 .IP 1
 Make sure that the formula and its negation are
 realizable by non-deterministic co-Büchi automata.
@@ -115,6 +114,7 @@ realizable by deterministic Büchi automata.
 Make sure that the formula is realizable
 by a weak and deterministic Büchi automata.
 .RE
+.RE
 
 .TP
 \fBSPOT_OOM_ABORT\fR
@@ -134,9 +134,12 @@ ignoring them), and setting this variable will interfer with that.
 Select the default algorithm that must be used to check the persistence
 or recurrence property of a formula f. The values it can take are 1
 or 2. Both methods work either on f or !f thanks to the duality of
-persistence and recurrence classes.
-See "https://spot.lrde.epita.fr/hierarchy.html" for more details. If
-it is set to:
+persistence and recurrence classes.  See
+.UR https://spot.lrde.epita.fr/hierarchy.html
+this page
+.UE
+for more details. If it is set to:
+.RS
 .RS
 .IP 1
 It will try to check if f (or !f) is co-Büchi realizable in order to
@@ -145,6 +148,7 @@ tell if f belongs to the persistence (or the recurrence) class.
 It checks if f (or !f) is det-Büchi realizable to tell if f belongs
 to the recurrence (or the persistence) class.
 .RE
+.RE
 
 .TP
 \fBSPOT_SATLOG\fR
@@ -202,6 +206,7 @@ variable should hold a value between 1 and 8, corresponding to the
 following tests described in our Spin'15 paper (see the BIBLIOGRAPHY
 section).  The default is 8.
 .RS
+.RS
 .IP 1
 sl(a) x sl(!a)
 .IP 2
@@ -219,6 +224,7 @@ sl(a) x sl(!a), performed on-the-fly
 .IP 8
 cl(a) x cl(!a)
 .RE
+.RE
 
 .TP
 \fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
diff --git a/bin/spot-x.cc b/bin/spot-x.cc
index 7225d751c..10acb4219 100644
--- a/bin/spot-x.cc
+++ b/bin/spot-x.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -43,7 +43,7 @@ static const argp_option options[] =
 (0) disables it, (1) enables rules based on syntactic implications, \
 (2) additionally allows automata-based implication checks, (3) enables \
 more rules based on automata-based implication checks.  The default value \
-depends on the --low/--medium/--high settings.") },
+depends on the --low, --medium, or --high settings.") },
     { nullptr, 0, nullptr, 0, "Translation options:", 0 },
     { DOC("ltl-split", "Set to 0 to disable the translation of automata \
 as product or sum of subformulas.") },