moglia
2010-05-13 0110094b2d206e88dceb0cfe2bc4c85f2e826dda
install/lib/install.lib.php
@@ -56,6 +56,10 @@
$FILE = realpath('../install.php');
//** Get distribution identifier
//** IMPORTANT!
//   This is the same code as in /server/mods-available/monitor_core_module.inc.php
//   So if you change it here, you also have to change it in
//   /server/mods-available/monitor_core_module.inc.php!
function get_distname() {
   
   $distname = '';