EOT;
}
function html_end() {
global $CONFIG;
$git = '/usr/bin/git';
$changelog = $CONFIG['webdir'].'/doc/CHANGELOG';
$version = 'v?';
if (file_exists($git) && is_dir($CONFIG['webdir'].'/.git')) {
chdir($CONFIG['webdir']);
$version = exec($git.' describe --tags');
} elseif (file_exists($changelog)) {
$changelog = file($changelog);
$version = explode(' ', $changelog[0]);
$version = 'v'.$version[0];
}
echo <<