Minor fix.
This commit is contained in:
parent
a9f85c9ab1
commit
6d6a1b284a
1 changed files with 1 additions and 1 deletions
|
@ -37,7 +37,7 @@
|
|||
% text will exceed the page boundary.
|
||||
\definecolor{background-color}{HTML}{EEEEFF}
|
||||
\let\oldtexttt\texttt%
|
||||
\renewcommand{\texttt}[1]{\colorbox{bgcolor}{\oldtexttt{#1}}}
|
||||
\renewcommand{\texttt}[1]{\colorbox{background-color}{\oldtexttt{#1}}}
|
||||
|
||||
% Box with background colour similar to web version:
|
||||
\newtcolorbox{agda}[1][]{
|
||||
|
|
Loading…
Reference in a new issue