+## ---------------- ##
+## doc/bison.help. ##
+## ---------------- ##
+
+# Some of our targets (cross-option.texi, bison.1) use "bison --help".
+# Since we want to ship the generated file to avoid additional
+# requirements over the user environment, we used not depend on
+# src/bison itself, but on src/getargs.c and other files. Yet, we
+# need "bison --help" to work to make help2man happy, so we used to
+# include "make src/bison" in the commands. Then we may have a
+# problem with concurrent builds, since one make might be aiming one
+# of its jobs at compiling src/bison, and another job at generating
+# the man page. If the latter is faster than the former, then we have
+# two makes that concurrently try to compile src/bison. Doomed to
+# failure.
+#
+# As a simple scheme to get our way out, make a stamp file,
+# bison.help, which contains --version then --help. This file can
+# depend on bison, which ensures its correctness. But update it
+# *only* if needed (content changes). This way, we avoid useless
+# compilations of cross-option.texi and bison.1. At the cost of
+# repeated builds of bison.help.
+
+EXTRA_DIST += $(top_srcdir)/doc/bison.help
+MAINTAINERCLEANFILES += $(top_srcdir)/doc/bison.help
+$(top_srcdir)/doc/bison.help: src/bison$(EXEEXT)
+ $< --version >doc/bison.help.t
+ $< --help >>doc/bison.help.t
+ $(top_srcdir)/build-aux/move-if-change doc/bison.help.t $@
+
+