diff --git a/doc/userdoc.org b/doc/userdoc.org index 963ae2df8f4a43f42d90327bd6dbe793be11629c..1547ebd6eee3789cfab19d4cb44c979970138292 100644 --- a/doc/userdoc.org +++ b/doc/userdoc.org @@ -12,7 +12,7 @@ #+ATTR_LATEX: :width 4cm #+HTML_HEAD_EXTRA: <style> pre.src-pugs:before { content: 'pugs'; } </style> #+HTML_HEAD_EXTRA: <style> pre.src-pugs-error:before { content: 'invalid pugs'; } </style> -#+HTML_HEAD_EXTRA: <style> .remark{ @extend .todo !optional;} </style> +#+HTML_HEAD_EXTRA: <style> .footref{ color: #2980b9; font-size: 100%; } </style> #+LATEX_CLASS_OPTIONS: [10pt] #+LATEX_HEADER: \usepackage[hmargin=2.5cm,vmargin=1.5cm]{geometry} #+LATEX_HEADER: \usepackage{ae,lmodern}