diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 2 | ||||
| -rwxr-xr-x | dev/tools/merge-pr.sh | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 87122e0fb5..f04de0ce6c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -209,7 +209,7 @@ ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_REF:=master}" +: "${bedrock2_CI_REF:=tested}" : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" : "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index c0a3eeb11c..a888998ebf 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -137,7 +137,8 @@ if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then else error "Local branch is not up-to-date with ${REMOTE}." error "Pull before merging." - ask_confirmation + # This check should never be bypassed. + exit 1 fi fi |