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?