software/theia: Make clone frontend names unique
- Loading...
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.
Check out, review, and merge locally
Step 1. Fetch and check out the branch for this merge request
git fetch "https://lab.nexedi.com/xavier_thompson/slapos.git" "fix/theia-resiliency-unique-frontend-clones" git checkout -b "xavier_thompson/slapos-fix/theia-resiliency-unique-frontend-clones" FETCH_HEAD
Step 2. Review the changes locally
Step 3. Merge the branch and fix any conflicts that come up
git fetch origin git checkout "origin/master" git merge --no-ff "xavier_thompson/slapos-fix/theia-resiliency-unique-frontend-clones"
Step 4. Push the result of the merge to GitLab
git push origin "master"
Note that pushing to GitLab requires write access to this repository.
Tip: You can also checkout merge requests locally by following these guidelines.
- You're only seeing other activity in the feed. To add a comment, switch to one of the following options.
Revert this commit
This will create a new commit in order to revert the existing changes.