[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