mirror of
https://github.com/php/web-php.git
synced 2026-03-23 23:02:13 +01:00
dd8d8bf863
This patch adds some missing newlines, trims some multiple redundant final newlines into a single one, and trims few redundant leading newlines. According to POSIX, a line is a sequence of zero or more non-'<newline>' characters plus a terminating '<newline>' character. [1] Files should normally have at least one final newline character. C89 [2] and later standards [3] mention a final newline: "A source file that is not empty shall end in a new-line character, which shall not be immediately preceded by a backslash character." Although it is not mandatory for all files to have a final newline fixed, a more consistent and homogeneous approach brings less of commit differences issues and a better development experience in certain text editors and IDEs. [1] http://pubs.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap03.html#tag_03_206 [2] https://port70.net/~nsz/c/c89/c89-draft.html#2.1.1.2 [3] https://port70.net/~nsz/c/c99/n1256.html#5.1.1.2
43 lines
1.1 KiB
PHP
43 lines
1.1 KiB
PHP
<?php
|
|
|
|
/*
|
|
This code redirects the user to the exact file to
|
|
download, and logs the download if it's something
|
|
we would like to know about (PHP binary or source).
|
|
*/
|
|
|
|
function get_actual_download_file($file)
|
|
{
|
|
// Could be a normal download or a manual download file
|
|
$possible_files = array($file => TRUE, "manual/$file" => FALSE);
|
|
|
|
// Find out what is the exact file requested
|
|
$found = FALSE;
|
|
foreach ($possible_files as $name => $log) {
|
|
if (@file_exists($_SERVER['DOCUMENT_ROOT'] . '/distributions/' . $name)) {
|
|
$found = $name;
|
|
break;
|
|
}
|
|
}
|
|
|
|
return $found;
|
|
}
|
|
// Download a file from a mirror site
|
|
function download_file($mirror, $file)
|
|
{
|
|
global $MYSITE;
|
|
|
|
// Redirect to the particular file
|
|
if (!headers_sent()) {
|
|
status_header(302);
|
|
header('Location: ' . $mirror . 'distributions/' . $file);
|
|
} else {
|
|
exit("Unable to serve you the requested file for download");
|
|
}
|
|
|
|
// Try to flush output, and make the browser really
|
|
// download the file, even if the log server is down
|
|
echo " ";
|
|
flush();
|
|
}
|