https://github.com/theia-ide/theia/issues/4027January 16, 2019 at 12:54pm
I think you wanted to work on the above issue. We would be happy if you have time, as we're quite swamped at this time.
January 17, 2019 at 7:10am
i will have a look at it, but only next week. If someone wants to work on it in the meantime. It is fine with me