Closed kevmoo closed 6 months ago
@Ephenodrom – you around?
@kevmoo sorry I have totally forgotten about this pr. Currently the Chrome pipeline seems to have some test failures. If this is fixed I will merge the PR and upload a new version on pub.dev.
@Ephenodrom it looks like timeouts. Could you hit the re-run button?
I'll validate locally...
@Ephenodrom – chrome passes IF you use -j 1
– so concurrency is causing the problems here.
@Ephenodrom – you're going to publish, right? Thanks so much!
@kevmoo Strange bug, the PR is marked as merged, but the changes are not in the master branch. Any idea ?
@Ephenodrom – looks like it rolled back? weird!!!
@dghgit Hello David, we have strange problem. It seems that the merged requests are rolled back. Any idea if this has something to do with the mirror ? I assume that this is NOT a generic github bug ...
@kevmoo FYI
@Ephenodrom did you merge into the backing repository? (You need to follow the command line instructions on the backing repo). Once the change is committed and pushed the mirror will pick it up, at the moment the mirror is showing this as the latest:
commit 59e06028bff338adc7d25ff9da4063a3b2e28b4c (HEAD -> master, origin/master, origin/HEAD)
Author: Ephenodrom <daniel@ephenodrom.de>
Date: Fri Apr 14 18:02:01 2023 +0200
Prepare release 3.7.2
This would be a chance to rebase and make a more clean commit, too!
@kevmoo Ok now i know how to merge it in the base repo. Any chance on reopening the PR or recreating the branch in your fork ?