Notes on how to add the port to $db_url

There is no clear way on how to add a non default port to the $db_url in settings.php. This patch adds a few lines that states how to do it.