Unable to save file with a '.txt' filename extension

Problem/Motivation

I exported a plaintext file with the filename 'email.txt' but the exported file has a filename 'email.txt.plaintext'

Steps to reproduce

1. Create an export display for a view.
2. Set the filename to whatever.txt
3. Save view.
4. Run the export, file is saved as 'whatever.txt.plaintext'

Proposed resolution

I'm not sure what the best approach would be. The first thing that comes to mind is to change line 12 in PlaintextEncoder.php from
protected static $format = 'plaintext';
to
protected static $format = 'txt';
But i'd rather avoid this type of patch just in case some people already have code that expects the 'plaintext' extension.

Or just create a new encoder that extends the PlaintextEncoder class and override the format.

What is the best approach?