From 632ce4aa44bd21e7cb599a6d89c75b6fca0033b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabian=20M=C3=BCller?= Date: Thu, 6 Nov 2014 06:35:23 +0100 Subject: [PATCH] Set the core_id preferences item at game launch. The id of the used core is set and saved if given as a command line interface. This commit makes use of the new "core" command line option. --- src/game_launcher.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/game_launcher.cpp b/src/game_launcher.cpp index 7c82c4dbe325..56f6fabf275b 100644 --- a/src/game_launcher.cpp +++ b/src/game_launcher.cpp @@ -139,6 +139,9 @@ game_launcher::game_launcher(const commandline_options& cmdline_opts, const char const std::string app_basename = filesystem::base_name(appname); jump_to_editor_ = app_basename.find("editor") != std::string::npos; + if (cmdline_opts_.core_id) { + preferences::set_core_id(*cmdline_opts_.core_id); + } if (cmdline_opts_.campaign) { jump_to_campaign_.jump_ = true; jump_to_campaign_.campaign_id_ = *cmdline_opts_.campaign;