diff options
| author | Hans Hagen <pragma@wxs.nl> | 2017-10-01 16:40:17 +0200 |
|---|---|---|
| committer | Context Git Mirror Bot <phg42.2a@gmail.com> | 2017-10-01 16:40:17 +0200 |
| commit | 80743fc19190334d3a0d4c86538663b98695a573 (patch) | |
| tree | 7a94f73a318e0362bacc2596ac8fc6201ed1d1b6 /tex/context/base/mkiv/font-pre.mkiv | |
| parent | 164a98ac4e58ae88de0a83d1eb60583827f4fbab (diff) | |
| download | context-80743fc19190334d3a0d4c86538663b98695a573.tar.gz | |
2017-10-01 14:38:00
Diffstat (limited to 'tex/context/base/mkiv/font-pre.mkiv')
| -rw-r--r-- | tex/context/base/mkiv/font-pre.mkiv | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/tex/context/base/mkiv/font-pre.mkiv b/tex/context/base/mkiv/font-pre.mkiv index b754714eb..632cbe29c 100644 --- a/tex/context/base/mkiv/font-pre.mkiv +++ b/tex/context/base/mkiv/font-pre.mkiv @@ -783,11 +783,15 @@ %D don't want huge switches to the main bodyfont and style, so %D here too we use a direct method. -\let\infofont \relax % satisfy dep checker -\let\infofontbold\relax % satisfy dep checker - -\definefont[infofont] [file:dejavusansmono at 6pt] % todo \the\everybodyfont -\definefont[infofontbold][file:dejavusansmono-bold at 6pt] % todo \the\everybodyfont +\let\infofont \relax +\let\infofontbold \relax +\let\smallinfofont \relax +\let\smallinfofontbold\relax + +\definefont[infofont] [file:dejavusansmono*none at 6pt] +\definefont[infofontbold] [file:dejavusansmono-bold*none at 6pt] +\definefont[smallinfofont] [file:dejavusansmono*none at 3pt] +\definefont[smallinfofontbold][file:dejavusansmono-bold*none at 3pt] %D Optimization (later we overload in math). Also needed in order to get \type {\ss} %D properly defined. |