test.py
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)