From: Ben Pfaff <blp@cs.stanford.edu>
Date: Sat, 22 Feb 2020 19:50:16 +0000 (+0000)
Subject: documentation: Fix build with some versions of makeinfo.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=90731b37a52eb7cf33cf0ead99e8d19ba9b2204b;p=pspp

documentation: Fix build with some versions of makeinfo.

Reported by Jeremy Lavergne.
---

diff --git a/doc/pspp-output.texi b/doc/pspp-output.texi
index 38c72d3aa7..4b9aeb203e 100644
--- a/doc/pspp-output.texi
+++ b/doc/pspp-output.texi
@@ -38,6 +38,13 @@ Each of these forms is documented separately below.
 @command{pspp-output} also has several undocumented command forms that
 developers may find useful for debugging.
 
+@menu
+* The pspp-output detect Command::
+* The pspp-output dir Command::
+* The pspp-output convert Command::
+* Input Selection Options::
+@end menu
+
 @node The pspp-output detect Command
 @section The @code{detect} Command