phpMyAdmin-ServerSelectDisplayName.patch

   1 --- phpMyAdmin-4.8.2-all-languages/libraries/classes/Server/Select.php~ 2018-06-21 20:08:17.000000000 +0300
   2 +++ phpMyAdmin-4.8.2-all-languages/libraries/classes/Server/Select.php  2018-08-13 12:00:56.105426801 +0300
   3 @@ -72,7 +72,7 @@
   4              if (!empty($server['verbose'])) {
   5                  $label = $server['verbose'];
   6              } else {
   7 -                $label = $server['host'];
   8 +                $label = isset($server['display']) ? $server['display'] : $server['host'];
   9                  if (!empty($server['port'])) {
  10                      $label .= ':' . $server['port'];
  11                  }