Add option to turn it on/off

This commit is contained in:
2023-10-29 23:09:09 +01:00
parent a105028f10
commit 32368f73ca
7 changed files with 39 additions and 11 deletions

View File

@ -42,6 +42,7 @@ export class Editor {
withLineNumbers!: Compartment;
vimModeCompartment!: Compartment;
hoveringCompartment!: Compartment;
completionsCompartment!: Compartment;
chosenLanguage!: Compartment;
dynamicPlugins!: Compartment;
currentDocumentationPane: string = "introduction";