feat: howto boxes, ci updates

2026-07-24 10:44:15 +02:00
parent 276348a957
commit 0ef8aca745
5 changed files with 326 additions and 314 deletions
@@ -107,3 +107,7 @@
    }%
    \par\smallskip
 }
+
+\newcommand\howto[2]{%
+    \coloredbox{gray}{\tr{\howtotextEN}{\howtotextDE}\ #1}{#2}%
+}