We just changed our MySQL servers and had to adjust the connection settings to use a different port.
I searched for instructions on how to do it and found the “How do I specify to use Mysql on a custom port or to connect Mysql over a socket?” FAQ
But it only says how to use a custom port for a new installation but not for an existing one.
After trying to manually add it into the host config option (which I now know doesn’t work) I had to go through the whole installation again. At least my existing data was preserved…
For anyone having the same problem: add a “port” config option to config.ini.php
host = "localhost"
port = 1234
I think this should be added to the FAQ. It can’t be required to delete the (manually edited) config file, run the installation again and then restoring the custom config for something as simple as a port change.