Email Gateway (Feb 23 2022 at 17:09): Email Gateway (Feb 23 2022 at 17:09):From: "Jakobitsch, Max-Julian" <Max-Julian.Jakobitsch@aau.at>
As mentioned on Zulip:
Marginal comments (\<comment>) are normally part of the LaTeX/PDF output,
but are left out when they appear after text (and some other markup
commands I have tried).
― <Marginal comments should appear in LaTeX, right?>
text<But apparently not after markup commands.>
― <I'm invisible!>
I discovered this while messing around with document preparation, and
suppose its impact on Isabelle users is quite limited.
It seems, however, like it is not intended behavior.
Regards,
Max Jakobitsch
smime.p7s
Last updated: Jul 15 2022 at 23:21 UTC