ed.texi to PDF

[Matt Wette]

I ran texi2any --pdf ed.texi and it failed.
This is on ed-1.16.
The following makes it work.

e$ diff -u ed.texi ed.texi-new
--- ed.texi    2020-02-20 04:57:27.000000000 -0800
+++ ed.texi-new    2020-11-27 12:04:35.539542583 -0800
@@ -45,6 +45,7 @@
 This manual is for GNU ed (version @value{VERSION}, @value{UPDATED}).
 @end ifnottex

+@ifnottex
 @menu
 * Overview::                        Overview of the @command{ed} command
 * Introduction to line editing::    Getting started with GNU @command{ed}
@@ -57,6 +58,7 @@
 * Problems::                        Reporting bugs
 * GNU Free Documentation License::  How you can copy and share this manual
 @end menu
+@end ifnottex

 @sp 1
 @insertcopying