Server names were also affected by bug #9021...

...(translated name not updated when switching language). But the
previous fix for this bug was canceled by a useless copy of
game_config values in preferences. So, fix and simplify the code by
removing it.
This commit is contained in:
Ali El Gariani 2007-09-26 14:27:40 +00:00
parent edd024007c
commit 0b9a5d45e9

View file

@ -148,21 +148,7 @@ void _set_iconize_list(bool sort)
const std::vector<game_config::server_info>& server_list()
{
static std::vector<game_config::server_info> pref_servers;
if(pref_servers.empty()) {
std::vector<game_config::server_info> &game_servers = game_config::server_list;
wassert(game_servers.size() > 0);
pref_servers.insert(pref_servers.begin(), game_servers.begin(), game_servers.end());
const std::vector<config *> &user_servers = get_prefs()->get_children("server");
std::vector<config *>::const_iterator server;
for(server = user_servers.begin(); server != user_servers.end(); ++server) {
game_config::server_info sinf;
sinf.name = (**server)["name"];
sinf.address = (**server)["address"];
pref_servers.push_back(sinf);
}
}
return pref_servers;
return game_config::server_list;
}
const std::string network_host()