Only allow merge requests to be merged to develop if the pipeline succeeds
We sometimes miss that the pipeline failed, see e.g., !260 (merged), !246 (merged). As a result, the develop
build fails, which is bad. We can configure that merge is only allowed when the pipeline succeeds, see: here.
what do you think?