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