editor: move docs toggle from settings

This removes the docs toggle switch from the settings and adds a new
docs toggle button to the editor.

Fixes: https://github.com/pybricks/support/issues/778
This commit is contained in:
David Lechner
2022-12-06 15:38:58 -06:00
committed by David Lechner
parent 55cf05d480
commit cc20ab8c35
8 changed files with 34 additions and 36 deletions
+7
View File
@@ -93,4 +93,11 @@
color: bp.$pt-dark-text-color-muted;
}
}
&-doc-button {
position: absolute;
bottom: bp.$pt-grid-size;
right: bp.$pt-grid-size;
z-index: bp.$pt-z-index-overlay;
}
}