From: Ben Pfaff <blp@cs.stanford.edu>
Date: Mon, 27 Jul 2015 05:04:27 +0000 (-0700)
Subject: dump: Title section sometimes has an extra 1 after 0x31.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=f7ab332bead0665caa4f3ccc7dcf28098f8b0406;p=pspp

dump: Title section sometimes has an extra 1 after 0x31.
---

diff --git a/dump.c b/dump.c
index a31cceae44..a7ccbdc88b 100644
--- a/dump.c
+++ b/dump.c
@@ -267,6 +267,7 @@ dump_value_31(FILE *stream)
           if (match_byte(0x31))
             {
               /* Only one example in the corpus. */
+              match_byte(1);
               match_byte(0);
               match_byte(0);
               match_byte(0);