Coverage: Fix newlines

diff --git a/coverage.php b/coverage.php
index dc668b4e414f2ed5029567a576d6e5dfd8776bea..5c1fa0b6c0ae69b17f95b4cef3a0ce0088bcc4ab 100644 (file)
--- a/coverage.php
+++ b/coverage.php
@@ -33,9 +33,10 @@ if (!extension_loaded("xdebug")) {
        // highlight single file
        $filename = $_GET["coverage"];
        $coverage = (file_exists($coverage_filename) ? unserialize(file_get_contents($coverage_filename)) : array());
-       $file = explode("\n", highlight_file($filename, true));
+       $file = explode("\n", substr(highlight_file($filename, true), 5, -6)); // unwrap <pre></pre>
        $prev_color = null;
        $s = "";
+       echo "<pre>";
        for ($l=0; $l <= count($file); $l++) {
                $line = $file[$l];
                $color = "#C0FFC0"; // tested
@@ -59,12 +60,13 @@ if (!extension_loaded("xdebug")) {
                        foreach (array_reverse($open_tags) as $tag) {
                                echo "</" . preg_replace('~ .*~', '', $tag) . ">";
                        }
-                       echo "</div>\n";
+                       echo "</div>";
                        $s = ($open_tags ? "<" . implode("><", $open_tags) . ">" : "");
                        $prev_color = $color;
                }
                $s .= "$line\n";
        }
+       echo "</pre>";
 } else {
        if (file_exists($coverage_filename)) {
                // display list of files