Eliminate a few unneeded match_bytes(0)s.

diff --git a/dump.c b/dump.c
index 8a2fbc4e5269e6c7a91279a3eb898d7c7964e066..854486fde4c1e08b802b0a153b06fc6eb3b55790 100644 (file)
--- a/dump.c
+++ b/dump.c
@@ -531,10 +531,6 @@ dump_title(void)
         {
           printf("footnote %d:\n", i);
           dump_footnote_value(0);
-          match_byte(0);
-          match_byte(0);
-          match_byte(0);
-          match_byte(0);
           if (match_byte (0x31))
             {
               /* Custom footnote marker string. */