Reinit docs to shrink git repo

This commit is contained in:
Mateusz Pusz
2024-11-05 18:52:17 +01:00
commit 32808bef78
1273 changed files with 1002503 additions and 0 deletions
+22
View File
@@ -0,0 +1,22 @@
div.example {
display: block;
margin-top: 5pt;
margin-bottom: 5pt;
font-size: 9pt;
}
div.note {
display: block;
margin-top: 5pt;
margin-bottom: 5pt;
font-size: 9pt;
}
div.note .texttt { font-size: 9pt; }
div.example .texttt { font-size: 9pt; }
div.note .textsf { font-family: 'Noto Sans'; font-size: 9pt; }
div.example .textsf { font-family: 'Noto Sans'; font-size: 9pt; }
div.note .math { font-size: 9pt; }
div.example .math { font-size: 9pt; }