[REF] tools: rename extras into tools

2025-10-06 19:59:41 +07:00 · 2019-06-09 16:56:27 +02:00
parent 2a19aeb6a3
commit e1bcea77b5
70 changed files with 32 additions and 31 deletions
@@ -0,0 +1,30 @@
+body {
+  font-family: sans-serif;
+}
+
+.title,
+.section {
+  width: 768px;
+  margin: auto;
+}
+
+.title div {
+  color: #333333;
+  font-style: italic;
+}
+
+.section {
+  background-color: #d5d5d5;
+  padding: 16px;
+  margin-top: 10px;
+  margin-bottom: 10px;
+}
+
+.links a {
+  margin: 10px 5px;
+}
+
+.benchmarks {
+  display: grid;
+  grid-template-columns: auto auto;
+}