mirror of
https://github.com/wesnoth/wesnoth
synced 2025-04-26 11:35:12 +00:00
f136bb9ef3
There has been functionality to manage custom servers in the player's preferences file since as far back as commit 5fb0b2a91123474d147c9de4918fc11a1b4c15ac in June 2007, but there's never been a user interface for it. This commit removes the current server list dialog attached to the MP Connect dialog and replaces it with the same functionality embedded into the latter, as well as the ability to edit the server list in the player's preferences file. There's some code movement in a few other places since the previous function in the preferences namespace doesn't suit the new code (it always returned a combined list of game and player-defined servers). There's some disabled code referencing a situation where the listbox with the list of servers allows the code (and the player) to clear the selection. It's disabled because there are some UX issues with it noted in the code comments associated to it. Fixes #4564.