Martin Henz

Fixed by https://github.com/source-academy/js-slang/pull/1232 but best check again in production once bumping js-slang has happened.

Reopening so that we remember to check the frontend, in Chrome and Firefox, after js-slang is bumped.

Hmm, anyone looking after this PR? @bnjmnt4n ? There is enthusiastic support from @angelsl . But still in draft and currently with merge conflict...

Reviewing our open PRs and this one comes up again. @bnjmnt4n do you have time these days? There is/was enthusiastic support from @angelsl . But still in draft and currently...

I don't think this is a good first issue, but it should be done. Any ideas welcome.

I think this proposal is simple and clear. Let's go ahead with it.

I'm quite interested in this. How would we present this to the users? Quite some time ago, someone floated the idea of a "Settings" menu item, along with "Help" and...

Thanks for the mock-up! I think such a drop-down menu would be much too prominent. Students would typically change their Ace mode three or four times max throughout the entire...

Regarding the goals: I'm adding "online" to the SA tagline: Immersive **online** experiential environment for learning programming The editor plays a central role in this aspiration, so your comments and...

Things are moving fast. We already have a profile page! We could have the following items as "Settings" in the profile page: * Ace keyboard shortcuts, with the selection "default",...