#!/usr/bin/env bash

set -e

# This script depends (at least) on git and jq.
# It should be used like this: dev/tools/merge-pr.sh /PR number/

#TODO: check arguments and show usage if relevant

PR=$1

CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD)
REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote")
git fetch "$REMOTE" "refs/pull/$PR/head"

API=https://api.github.com/repos/coq/coq

BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label')

COMMIT=$(git rev-parse FETCH_HEAD)
STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state')

if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then
  echo "Wrong base branch"
  read -p "Bypass? [y/N] " -n 1 -r
  echo
  if [[ ! $REPLY =~ ^[Yy]$ ]]
  then
    exit 1
  fi
fi;

if [ "$STATUS" != "success" ]; then
  echo "CI status is \"$STATUS\""
  read -p "Bypass? [y/N] " -n 1 -r
  echo
  if [[ ! $REPLY =~ ^[Yy]$ ]]
  then
    exit 1
  fi
fi;

git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e

# TODO: improve this check
if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then
  echo "******************************************"
  echo "** WARNING: does this PR have overlays? **"
  echo "******************************************"
fi