jeans/arduino-ide
1
0
Fork 0
mirror of https://github.com/arduino/arduino-ide.git synced 2025-11-24 01:26:10 +00:00
Code Issues Packages Projects Releases Wiki Activity

fixed save-as. added sketchload

Browse Source 
Signed-off-by: Akos Kitta <kittaakos@typefox.io>
This commit is contained in:
Akos Kitta
2020-07-30 19:58:14 +02:00
parent 528f4150d3
commit 8ab70f48f8
19 changed files with 360 additions and 114 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
arduino-ide-extension/src/browser/theia/editor/editor-manager.ts
View File

@@ -17,7 +17,9 @@ export class EditorManager extends TheiaEditorManager {
const { editor } = widget;
if (editor instanceof MonacoEditor) {
const codeEditor = editor.getControl();
codeEditor.updateOptions({ readOnly });
const lineNumbersMinChars = 2;
const overviewRulerLanes = 0;
codeEditor.updateOptions({ readOnly, lineNumbersMinChars, overviewRulerLanes });
}
}
return widget;