install/lib/install.lib.php
@@ -57,7 +57,7 @@ //** Get distribution identifier //** IMPORTANT! // This is the same code as in server/mods-available/monitor_core_module.inc.php // This is the same code as in server/lib/classes/monitor_tools.inc.php // So if you change it here, you also have to change it in there! function get_distname() {
