diff --git a/doc/download_all.php b/doc/download_all.php index 3b6c808bd5..051a4ba7d9 100644 --- a/doc/download_all.php +++ b/doc/download_all.php @@ -11,17 +11,18 @@ // platform=x show only versions for platform x (win/mac/linux/solaris) require_once("docutil.php"); +require_once("versions.inc"); $xml = $_GET["xml"]; $dev = $_GET["dev"]; -if (!$xml) $dev=1; $pname = $_GET["platform"]; $min_version = $_GET["min_version"]; $max_version = $_GET["max_version"]; $version = $_GET["version"]; $type_name = $_GET["type"]; +$client_info = $_SERVER['HTTP_USER_AGENT']; -require_once("versions.inc"); +if (!$xml) $dev=1; function dl_item($x, $y) { echo "