clime wrote:
> So if some other maintainer pushes his work to the server meanwhile,
> this will just delete his work? Or what's the idea here?
I guess the safe thing to do would be to wait and see whether that commit
also fails to build (i.e., if the CI build fails, check whether the built
commit is still the current HEAD, and trigger the revert only if it is,
otherwise defer the decision to the new HEAD's CI build), but if that is the
case, yes, it will definitely be deleted from the server. But it will still
be present in the maintainer's local checkout and can be trivially pushed
back together with a build fix.
Kevin Kofler
_______________________________________________
devel mailing list -- devel@xxxxxxxxxxxxxxxxxxxxxxx
To unsubscribe send an email to devel-leave@xxxxxxxxxxxxxxxxxxxxxxx
Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/
List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines
List Archives: https://lists.fedoraproject.org/archives/list/devel@xxxxxxxxxxxxxxxxxxxxxxx
