#718: Delete config-info before reconfiguring with an option list ------------------------+--------------------------------------------------- Reporter: eschnett | Owner: eschnett Type: defect | Status: new Priority: major | Milestone: Component: SimFactory | Version: Keywords: | ------------------------+--------------------------------------------------- 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.