When saving a file under a user-provided name, we check the name for any extension. If there is no extension or if the extension is not one of the allowed extensions for the chosen file format, we forcibly append an allowed extension to the filename.
This commit updates this behaviour to append an extension only in the case where there is no extension. If the user-provided filename already has an extension, we keep it as it is even if we don't recognize the extension.
When saving a file under a user-provided name, we check the name for any extension. If there is no extension or if the extension is not one of the allowed extensions for the chosen file format, we forcibly append an allowed extension to the filename.
This commit updates this behaviour to append an extension only in the case where there is no extension. If the user-provided filename already has an extension, we keep it as it is even if we don't recognize the extension.
closes #1087.