Fabian Homborg b5cbdc623d docs/tutorial: Replace coloring markup ...

This used to use doxygen's html blocks, which don't have a *direct*
equivalent in sphinx in code blocks.

Instead of adding this to the pygments highlighter, let's just use
some roles.

It's a teensy bit awkward as we then use block styling, but we want to
add more of our own styling anyway, so we can presumably get this
somehow, and these html tags look awkward and confuse people.

Fix #6640

[ci skip]

2020-02-22 18:01:05 +01:00

..

custom.css

We no longer have two doc systems, move sphinx_doc_src back to doc_src

2020-02-19 17:00:35 -08:00

pygments.css

docs/tutorial: Replace coloring markup

2020-02-22 18:01:05 +01:00