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 Brigit Murtaugh (@bamurtaugh) Alessandro (Ale) Segala (@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 Benjamin Pasero (@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]

Alessandro (Ale) Segala (@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...