No, my problem with the git integration wasn't the editor or whatever. It was that if I made a change, I had to commit and push it (and I'm new to Javascript, s

No, my problem with the git integration wasn't the editor or whatever. It was that if I made a change, I had to commit and push it (and I'm new to Javascript, so I make a lot of minor errors) so my time was spent writing "fix typo" commit messages. And even when I did do that, it often wouldn't notice my push for many minutes on the Screeps side of things. I never really figured out how to reliably get it to pick up my changes, so I'd try refreshing the webpage, etc. to get it. I.e. the github integration was too poor to be useful, at least back when I tried it and in the way I was using it. Plus, there was no way to go the other direction: edit something online and then push to github. You could only go the other way.