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?
- 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?
Thanks,
Alan
--
OpenPGP Key ID : 040D0A3B4ED2E5C7
Athmospheric CO₂ (Updated February 4, 2016, Mauna Loa Obs.): 403.08 ppm
signature.asc
Description: PGP signature
