@piggo And if you really crave that web editor, I guess WebIDE of guthub (not clue whether such a thing exists, but I guess it does), or WebIDE of gitlab (works well!) could serve you just about fine. No need for a specific system, you can hack this together from existing pieces out there.