From 868335409d48eb6ab24a64f83fd6ab798f57b897 Mon Sep 17 00:00:00 2001
From: ZhilkinSerg <ZhilkinSerg@users.noreply.github.com>
Date: Thu, 30 Jan 2020 11:55:41 +0300
Subject: [PATCH] Don't add duplicate options to the page

---
 src/options.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/options.cpp b/src/options.cpp
index 805dcaaade941..57452769d453b 100644
--- a/src/options.cpp
+++ b/src/options.cpp
@@ -135,7 +135,14 @@ void options_manager::addOptionToPage( const std::string &name, const std::strin
 {
     for( Page &p : pages_ ) {
         if( p.id_ == page ) {
+            // Don't add duplicate options to the page
+            for( const cata::optional<std::string> &i : p.items_ ) {
+                if( i.has_value() && i.value() == name ) {
+                    return;
+                }
+            }
             p.items_.emplace_back( name );
+            return;
         }
     }
     // @TODO handle the case when an option has no valid page id (note: consider hidden external options as well)