add github pages site

2025-09-13 14:31:15 +00:00 · 2023-11-02 21:44:14 +01:00
parent 35939c92c9
commit faf454f649
18 changed files with 763 additions and 1 deletions
--- a/docs/stylesheets/extra.css
+++ b/docs/stylesheets/extra.css
@@ -0,0 +1,49 @@
+/* This file is used for extra styles that are not part of the theme */
+
+span.title {
+  font-weight: bold;
+}
+
+span.em {
+  font-weight: bold;
+}
+
+.separator {
+  border-bottom: 1px solid #e3e8ee;
+}
+
+a.field {
+  font-weight: 600;
+  /* color: #3c4257; */
+  font-size: .8rem;
+}
+
+span.parent-field {
+  font-weight: 600;
+  color:#a3acb9;
+  font-size: .85em;
+}
+
+span.type {
+  color: #8792a2;
+  font-size: .7rem;
+  margin-right: 4px;
+}
+
+span.version {
+  color: #8792a2;
+  font-size: .7rem;
+  float: right;
+}
+
+span.faint {
+  color: #8792a2;
+}
+
+.md-social__link svg {
+  fill: rgb(61, 61, 61);
+}
+
+.md-tabs__link {
+  font-size: 0.8rem;
+}