From: Ben Pfaff <blp@cs.stanford.edu>
Date: Mon, 27 Jul 2015 05:03:53 +0000 (-0700)
Subject: dump: Title section sometimes uses font size 14, not just 12.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=2a52e76a21ea61ff2591a952b3d17d0ff355f6c0;p=pspp

dump: Title section sometimes uses font size 14, not just 12.
---

diff --git a/dump.c b/dump.c
index 90c32bf64d..a31cceae44 100644
--- a/dump.c
+++ b/dump.c
@@ -274,7 +274,8 @@ dump_value_31(FILE *stream)
               get_string();     /* foreground */
               get_string();     /* background */
               get_string();     /* font */
-              match_byte_assert(12); /* size? */
+              if (!match_byte(14))
+                match_byte_assert(12); /* size? */
             }
           else
             match_byte_assert(0x58);