wp-options.php ignores port for mysql when database is localhost

[carles_mateo]

According to documentation (​https://codex.wordpress.org/Editing_wp-config.php) this should work:
define( 'DB_HOST', 'localhost:3307' );

But instead, the port section is ignored and default mysql port is used.

But if I do:
define( 'DB_HOST', '127.0.0.1:3307' );

Then it works and connects to 3307.

I've checked with two different systems, with the last WP version (English).

[carles_mateo]

Sample of the line in wp_config.php affected

[kitchin]

PHP treats localhost differently than 127.0.0.1.

Whenever you specify "localhost" or "localhost:port" as server, the MySQL client library will override this and try to connect to a local socket (named pipe on Windows). If you want to use TCP/IP, use "127.0.0.1" instead of "localhost". If the MySQL client library tries to connect to the wrong local socket, you should set the correct path as in your PHP configuration and leave the server field blank.

​http://php.net/mysql_connect
See also the comment at ​http://php.net/manual/en/mysqli.construct.php

I'll take a go at the codex.