Jörg, please note discouraged != disallowed :-)
I don't think we should complicate things to much with bots, protected
branches and alike ...
Am 25.03.22 um 09:46 schrieb jkubitz-ecli...@gmx.de:
Well, if direct pushing to the repository is disallowed it should be
disabled. I accidently made my first error with not creating a PR. And
got nor error message. Highly confusing.
If possible the error message should provide a link to a how-to-contribute.
Jörg
_______________________________________________
platform-dev mailing list
platform-dev@eclipse.org
To unsubscribe from this list, visit
https://www.eclipse.org/mailman/listinfo/platform-dev
_______________________________________________
platform-dev mailing list
platform-dev@eclipse.org
To unsubscribe from this list, visit
https://www.eclipse.org/mailman/listinfo/platform-dev
