Enable smart punctuation

[VojtechStep]

Turns -- and --- to ndash and mdash, respectively, and automatically inserts paired quotation marks; see https://rust-lang.github.io/mdBook/format/markdown.html#smart-punctuation.

Note that the option is called curly-quotes in the version of mdbook we use. In later versions it's called smart-punctuation.

[fredrik-bakke]

Note that the option is called curly-quotes in the version of mdbook we use. In later versions it's called smart-punctuation.

Could you add this as a comment in the .toml?

[VojtechStep]

I can do that tomorrow, though I don't think it's necessary, since curly-quotes will remain a deprecated alias in future version of mdbook, with a printed warning, so it's not going to silently break when we update

[fredrik-bakke]

I have another concern about this since the configuration name changed in mdbook 4.38 and I'm using a later* version locally. Does that mean I have to downgrade my version of mdbook? Would it be reasonable/possible to just update our mdbook version so that we don't have to worry about this in the future?

[fredrik-bakke]

Never mind, I see in their changelog that they are keeping the old name around for now.

[fredrik-bakke]

I've enabled auto-merge 👍

[VojtechStep]

Would it be reasonable/possible to just update our mdbook version

Of course eventually we want to upgrade, but we need to update our changes to the files in theme/ to match the new version, since mdbook sometimes breaks those. IIRC last time we tried to "just update our mdbook version" the navigation buttons and left ToC stopped working, and nobody's yet invested the necessary time to fix it, so we're keeping the version of mdbook and its plugins pinned to an older version