No duplicate inclusion of the same option in configuration files

[PhilippWendler]

In order to avoid ambiguities, the configuration parser avoids depending on the order of configuration statements. For example, included configuration options are always overwritten by configuration options in the including file, no matter the order of the option and the #include statement.

An exception for this is if there are two #include statements, both of which include a file with the same option. Then one takes precedence, which can be confusing for the user, because in order to find out whether an option from an included file is overwritten, all other included files need to be searched through transitively.

Thus the parser should reject duplicate different values of options from different included files. The user would have to manually specify the final value of the option in the including file.