changeset 5243 | 46a3f1348d4d |
parent 5239 | 2e753de86174 |
child 5255 | 2f3abe6fa8a3 |
--- a/test.py Wed Sep 23 15:35:26 2009 -0700 +++ b/test.py Wed Sep 23 15:38:36 2009 -0700 @@ -233,7 +233,7 @@ for example in dom.getElementsByTagName("Example"): f.write("<tr>\n") result = get_node_text(example.getElementsByTagName("Result")[0]) - if result == "FAIL": + if result in ["FAIL", "CRASH"]: f.write("<td style=\"color:red\">%s</td>\n" % result) else: f.write("<td style=\"color:green\">%s</td>\n" % result)