diff --git a/install/lib/install.lib.php b/install/lib/install.lib.php
index 8793dba028874b059ddeb693f4643eea9310cebd..b6ad9a7f23608ae7ecb703db6256c6b7d0534422 100644
--- a/install/lib/install.lib.php
+++ b/install/lib/install.lib.php
@@ -57,9 +57,8 @@ $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!
+//   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 there!
 function get_distname() {
 	
 	$distname = '';