# HG changeset patch
# User Franz Glasner <fzglas.hg@dom66.de>
# Date 1778869451 -7200
# Node ID 29826707b7daf4c32ceef714290b7c21fa9d24a4
# Parent  e363dc537be52a3ceb84fbf9bbe0f5821dcbe179
Comment

diff -r e363dc537be5 -r 29826707b7da docs/_latex/my-doc-fonts.sty
--- a/docs/_latex/my-doc-fonts.sty	Fri May 15 20:23:03 2026 +0200
+++ b/docs/_latex/my-doc-fonts.sty	Fri May 15 20:24:11 2026 +0200
@@ -32,7 +32,8 @@
 
 % A key compatible with options processing as option "fonts" but choices.
 \define@choicekey*{my-doc-fonts.sty}{fonts}[\val\nr]{%
-  default,   % do not change anything: deactivate the default dejavusansmono
+  % do not change anything: just deactivate the default "dejavusansmono"
+  default,
   % no augmentation needed: all characters available
   dejavusansmono,  % use DejaVu Sans Mono as monospaced font
   % the fonts below are augmented for missing characters