software/theia: Make theiaN frontend names unique
This concerns a case of resiliency in Theia: when a resilient Theia requests multiple import clones (by default only one is requested), e.g. when theia0 (export) has two import clones theia1 and theia2. Each clone requests a frontend for their theia service, which allows the Theia editor of the clone to be accessed without doing a takeover. Before this, all the import clones would request a frontend with the same name. This meant that only one frontend was allocated and might randomly redirect to one of the backup clones. See merge request !1481
Showing
Please register or sign in to comment