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 is a JavaScript interpreter for low-power Microcontrollers. This site is both a support community for Espruino and a place to share what you are working on.
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?