Simpler <title> string and default PDF filename

[mgkuhn]

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.)

[fonsp]

Thanks for the suggestion! Implemented in the upcoming release

[fonsp]

Do you have more suggestions for Pluto?

[mgkuhn]

Do you have more suggestions for Pluto?

Well ... since you asked: #2713