Closed planger closed 4 years ago
Right, good idea! Just not sure whether other Sprotty users will have use cases where the URI is not compatible with the navigator. But let's see. I've opened the PR against sprotty-theia: https://github.com/eclipse/sprotty-theia/pull/44/
Let's hold off this PR until we know whether this should go into sprotty directly.
Merged https://github.com/eclipse/sprotty-theia/pull/44 instead.
Fixes #385