Fix do not ping name of server

2019-11-27 11:38:30 +01:00
parent 9a9a43fc4d
commit c22fea52e5
3 changed files with 8 additions and 4 deletions
--- a/htdocs/core/lib/functions2.lib.php
+++ b/htdocs/core/lib/functions2.lib.php
@@ -1569,7 +1569,7 @@ function dol_print_reduction($reduction, $langs)
 */
 function version_os($option = '')
 {
-	if ($option) $osversion = php_uname($option);
+	if ($option == 'smr') $osversion = php_uname('s').' '.php_uname('m').' '.php_uname('r');
 	else $osversion = php_uname();
    return $osversion;
 }