diff -r 000000000000 -r eb3c7813b67a misc/katex-header.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/misc/katex-header.html Thu Dec 01 23:07:35 2022 +0200 @@ -0,0 +1,15 @@ + + + +