Make dump_footnote_value() more like dump_value().

diff --git a/dump.c b/dump.c
index bcb6d82dfd01bbdebc3b94f80c0f9d309060eaed..ede89f96ec14f758c8ee18bf77564575811ef3a3 100644 (file)
--- a/dump.c
+++ b/dump.c
@@ -788,10 +788,6 @@ dump_footnote_value(int level)
       match_byte (0);
       match_byte (0);
       match_byte (0);
-      match_byte (0);
-      match_byte (0);
-      match_byte (0);
-      match_byte (0);
     }
   else if (match_byte (4))
     {
@@ -810,7 +806,6 @@ dump_footnote_value(int level)
       match_byte (0);
       match_byte (0);
       match_byte (0);
-      match_byte (0);
     }
   else if (match_byte (1))
     {