On Mon, Jun 19, 2017 at 07:54:03PM +0200, Jürgen Spitzmüller wrote: > > Again: Why do we need the toolbar button? Why not let the document > itself ask for shell-escaping, depending on the need for that (e.g., > minted)?
Because we don't know whether it's needed? -- Enrico
