Hello,
Alan Schmitt <alan.schm...@polytechnique.org> writes:
> Hello,
>
> I see that
>
> src_coq[:exports code]{nat}
>
> exports to (latex export with minted)
>
> \mint{coq}~nat~
>
> which does not work as inline code here. The following would work,
> however, with a recent minted:
>
> \mintinline{coq}{nat}
>
> I have two questions:
> - should we support this and generate this code?
Sure. Could you provide and apply a patch for that?
> - in the meantime, I created a macro that does this for latex, but it
> does not work for html (it exports the “src_coq” string verbatim):
> #+macro: coq @@latex:\mintinline{coq}{$1}@@@@html:src_coq[:exports code]{$1}@@
> Why is this macro wrong?
Contents of an export snippet, e.g. @@html:...@@ are not evaluated by
the back-end. IOW this is back-end code.
Regards,
--
Nicolas Goaziou
