I've now added a branch protection rule for the github mirror, so that one can no longer push directly to it (so it's a true mirror now). The sageb0t user got an exemption so the sync from trac to the github mirror should still work (I've tested it for with a few commits).
Now if someone tries to push directly to the github mirror the following error message is shown remote: error: GH006: Protected branch update failed for refs/heads/public/build/gitpod_trac_tracking. remote: error: Changes must be made through a pull request. To https://github.com/sagemath/sagetrac-mirror.git ! [remote rejected] public/build/gitpod_trac_tracking -> public/build/gitpod_trac_tracking (protected branch hook declined) error: failed to push some refs to 'https://github.com/sagemath/sagetrac-mirror.git' Let me know if you experience any issues with this setup and I'll try to fix it promptly. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/a2da70b1-2aa6-4c6e-837b-908c4b639f08n%40googlegroups.com.
