Downloading a file with no extension from browser automatically adds ".txt"

[isidorn]

When downloading the compiled file (.out/app) in step 6, the downloaded file on my laptop is called app.txt. Something added the .txt extension automatically.

I'm using Edge 88 on macOS.

from @bamurtaugh @ItalyPaleAle

[isidorn]

I investigated into this and this is just how Chrome (and thus Edge) behaves and I am not sure if we can introduce a workaround for this.
Since in this case we fall back to the simple download operation here

More about how chrome handles this can be found here https://developers.google.com/web/updates/2011/08/Downloading-resources-in-HTML5-a-download

So in short, we fall back to Chrome and Chrome decides to add .txt to a file with no extension

fyi @bpasero

[ItalyPaleAle]

Do you think it might make sense to create an archive (like a ZIP) of all files downloaded from Codespaces? This would not just solve the issue of the extension, but would also make the download potentially smaller, and would fix other issues like #112099

Just a thought :)

[isidorn]

@ItalyPaleAle might make sense. Other software usually downloads as zip when there is more than one file to download.
If a user is just downloading one file, then putting it in a zip might just add one extra step...

[vscodenpa]

We closed this issue because we don't plan to address it in the foreseeable future. If you disagree and feel that this issue is crucial: we are happy to listen and to reconsider.

If you wonder what we are up to, please see our roadmap and issue reporting guidelines.

Thanks for your understanding, and happy coding!

[WRFan]

well, you may have closed the issue, but the issue with Edge appending .txt to files without an extension is not solved by that. I actually have to fall back to IE to download such files. Seems you have buried IE a little too early