Delete config-info before reconfiguring with an option list
Issue #718
new
The file config-info contains information about how the current configuration was configured. When re-configuring with a new option list, this file should be deleted, so that no information from the previous configuration can survive accidentally.
Keyword: