Ok, shift-enter sounds good. I'll make the change.
re: 'Web-Ide's show/hide "right side"' - not quite sure what you mean? Alt/Alt-Gf + F doesn't seem to do anything for me. Ctrl-F goes fullscreen which might be what you mean? I'm not sure how that can get confused with AltGr though?
Oh, looks like it's a Native Ide only thing.
If I connect to a device, go to the left side (terminal) and hit AltGr-F, it does the same as if I hit CTRL-F. But only the Native Ide, assumed it does the same everywhere. I'm on win 10...
© Espruino, powered by microcosm.
Report a problem