Don't concurrently build two versions of 'develop'

We just had two commits to develop being built close to each other (one started one minute after the other). The second one failed to deploy the nightly release, since just between the checkout and the push, the first build already pushed and thus the local checkout of the second build is outdated:

10:16:53  + rm -rf deploy/www/nightly
10:16:53  + mkdir -p deploy/www/nightly
10:16:53  + unzip -q releng/org.eclipse.escet.releng.website/target/eclipse-escet-nightly-20240704-071323-website.zip -d deploy/www/nightly/
10:16:54  + cd deploy/www
10:16:54  + grep -Fxq nightly .versions
10:16:54  + git config user.email escet-bot@eclipse.org
10:16:54  + git config user.name genie.escet
10:16:54  + git config push.default simple
10:16:54  + git add -A
10:16:57  + git commit -q -m 'Website release nightly.' -m 'Generated from commit 1101682715a80bb433e36de0f8cb5f7571f3ddab.'
10:16:57  + git push
10:16:59  To gitlab.eclipse.org:eclipse/escet/escet-website.git
10:16:59   ! [rejected]            master -> master (fetch first)
10:16:59  error: failed to push some refs to 'gitlab.eclipse.org:eclipse/escet/escet-website.git'
10:16:59  hint: Updates were rejected because the remote contains work that you do
10:16:59  hint: not have locally. This is usually caused by another repository pushing
10:16:59  hint: to the same ref. You may want to first integrate the remote changes
10:16:59  hint: (e.g., 'git pull ...') before pushing again.
10:16:59  hint: See the 'Note about fast-forwards' in 'git push --help' for details.
[Pipeline] }

We should limit concurrent builds for the same branch.

According to https://stackoverflow.com/a/41516843, we can just add the following to our Jenkinsfile:

pipeline {
    options {
        disableConcurrentBuilds()
    }
}