[m-rev.] for post-commit review: fix github issue #85

[Peter Wang]

On Tue, 24 Mar 2020 17:35:09 +1100 (AEDT), "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 
> On Tue, 24 Mar 2020 17:30:16 +1100 (AEDT), Julien Fischer <jfischer at opturion.com> wrote:
> > Quote `disable_warnings` there, we want it to emitted as <code> in HTML.
> 
> OK, I have done both of those things, but this aroused my curiosity.
> 
> +        disable_warnings [no_solution_disjunct] (
> +           Goal
> +        )
> 
> What causes indented code blocks like this to be emitted as <code>?

Indenting by four spaces introduces a code block in Markdown.

Peter