search

judge0 / ide

✨ Simple, free and open-source online code editor.
https://ide.judge0.com
MIT License
818 stars 257 forks source link

Change the filename of source code #20

Closed mamat-rahmat closed 5 years ago

mamat-rahmat commented 5 years ago

Currently, if we download the source code the filename always main.{ext} It would be nice if we can change the filename in the editor

hermanzdosilovic commented 5 years ago

Hi @mamat-rahmat,

I am not sure but I think that your browser can do that for your if it asks you where do you want to save your file. Check for your browser settings please.