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

Zoltan Somogyi zoltan.somogyi at runbox.com
Tue Mar 24 17:35:09 AEDT 2020



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>?

Zoltan.




More information about the reviews mailing list