diff --git a/doc/download_all.php b/doc/download_all.php index 5c1e778f03..6cdb7c8a64 100644 --- a/doc/download_all.php +++ b/doc/download_all.php @@ -166,13 +166,15 @@ if ($pname && $version) { if ($xml) { header('Content-type: text/xml'); - echo " - + echo "\n +\n "; foreach($platforms as $short_name=>$p) { show_platform_xml($short_name, $p, $dev); } - echo "\n"; + echo " +\n +"; } else { if ($pname) { $p = $platforms[$pname];