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

diff --git a/dump.c b/dump.c
index 90c32bf64d89a2245fdf33ce7ccce0ef4663ff8d..a31cceae4409a7700dc1ea3cf4dab9ff43d0eb4c 100644 (file)
--- 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);