diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index f89363aa1..fb8026399 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -287,6 +287,14 @@ header-item: "States:" INT } | "properties:" properties | HEADERNAME header-spec + { + char c = (*$1)[0]; + if (c >= 'A' && c <= 'Z') + error(@$, "ignoring unsupported header \"" + *$1 + ":\"\n\t" + "(but the capital indicates information that should not" + " be ignored)"); + delete $1; + } ap-names: | ap-names ap-name ap-name: STRING diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index b11a19a98..30da7963c 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -523,3 +523,40 @@ State: 1 [0] 0 --END-- EOF + + +cat >input <expected <