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.)
Reproduce:
Pluto.run(notebook="assignment1.jl")
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 theassignment1.pdf
that I would have naturally expected for the PDF version ofassignment1.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.)