Description
Reproduce:
Pluto.run(notebook="assignment1.jl")- export as PDF
Expected behaviour: default PDF filename assignment1.pdf
Actual behaviour: default PDF filename 🎈 assignment1.jl — Pluto.jl.pdf
If my notebook is simply called assignment1.jl, then Pluto currently sets in the DOM header <title>🎈 assignment1.jl — Pluto.jl</title> and as a result, if I export the notebook into a PDF, then the default filename that I'm offered by the browser (e.g. in Firefox on Ubuntu 20.04) is the rather awkward “🎈 assignment1.jl — Pluto.jl.pdf” taken from the <title>.
Suggestion: if instead the DOM had just <title>assignment1</title>, i.e. the notebook filename without the .jl suffix, then the default PDF export filename offered by the browser would simply be the assignment1.pdf that I would have naturally expected for the PDF version of assignment1.jl.
(I know balloons are very important, but arguably so are filenames that are easy to use on the command line, e.g. by students when they submit their homework as a Pluto-exported PDF.)