From: Ben Pfaff <blp@cs.stanford.edu>
Date: Fri, 7 Nov 2014 06:59:32 +0000 (-0800)
Subject: Eliminate a few unneeded match_bytes(0)s.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pspp;a=commitdiff_plain;h=82f10fa1c692b8f9e312312cffe6d63bd2518f6a

Eliminate a few unneeded match_bytes(0)s.
---

diff --git a/dump.c b/dump.c
index 8a2fbc4e52..854486fde4 100644
--- 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. */