diff --git a/genhtml.patch b/genhtml.patch index e407512c48..9f117304d1 100644 --- a/genhtml.patch +++ b/genhtml.patch @@ -1,5 +1,5 @@ ---- genhtml_ori 2013-07-06 20:45:58.973043561 +0200 -+++ genhtml 2013-07-06 20:46:22.473043550 +0200 +--- genhtml_ori 2013-07-10 19:23:55.041055126 +0200 ++++ genhtml 2013-07-10 19:31:39.041172541 +0200 @@ -2351,7 +2351,8 @@ ($year, $month, $day) = (localtime())[5, 4, 3]; @@ -10,3 +10,34 @@ } +@@ -3807,9 +3808,10 @@ + } else { + $class = "branchCov"; + $text = " + "; +- $title = "Branch $br_num was taken $taken ". +- "time"; +- $title .= "s" if ($taken > 1); ++ #$title = "Branch $br_num was taken $taken ". ++ # "time"; ++ #$title .= "s" if ($taken > 1); ++ $title = "Branch $br_num was taken X times"; + } + $current .= "[" if ($open); + $current .= ""; +@@ -3892,6 +3894,8 @@ + $count_format = format_count($count, $count_field_width); + } + else { ++ # force to 1 to avoid huge diffs between runs ++ $count = 1; + $result = $count; + $source_format = ''; + $count_format = format_count($count, $count_field_width); +@@ -5127,6 +5131,7 @@ + $countstyle = "coverFnLo"; + } else { + $countstyle = "coverFnHi"; ++ $count = "X"; + } + + write_html(*HTML_HANDLE, <