diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh | 8 | ||||
| -rw-r--r-- | dev/doc/changes.md | 5 | ||||
| -rw-r--r-- | dev/doc/xml-protocol.md | 4 | ||||
| -rwxr-xr-x | dev/tools/backport-pr.sh | 43 |
4 files changed, 52 insertions, 8 deletions
diff --git a/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh b/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh new file mode 100644 index 0000000000..9c4c905fa6 --- /dev/null +++ b/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=rm-campl4-remains + +if [ "$CI_PULL_REQUEST" = "7898" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + pidetop_CI_BRANCH="$_OVERLAY_BRANCH" + pidetop_CI_GITURL=https://github.com/ppedrot/pidetop + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 6d5023405a..1eea2443fe 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -88,6 +88,11 @@ Primitive number parsers have been split over three files (plugins/syntax/positive_syntax.ml, plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml). +Parsing + +- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules + Pcoq.Entry and Pcoq.Parsable were introduced to replace it. + ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index b35571e9ca..48671c03b6 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -10,9 +10,9 @@ versions of Proof General. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). -OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). +OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml). -Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt). +Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md). * [Commands](#commands) - [About](#command-about) diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index 5205350a61..9864fd4d69 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -1,11 +1,34 @@ #!/usr/bin/env bash -# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging] - set -e -PRNUM=$1 -OPTION=$2 +if [[ $# == 0 ]]; then + echo "Usage: $0 [--no-conflict] [--no-signature-check] [--stop-before-merging] prnum" + exit 1 +fi + +while [[ $# -gt 0 ]]; do + case "$1" in + --no-conflict) + NO_CONFLICTS="true" + shift + ;; + --no-signature-check) + NO_SIGNATURE_CHECK="true" + shift + ;; + --stop-before-merging) + STOP_BEFORE_MERGING="true" + shift + ;; + *) + if [[ "$PRNUM" != "" ]]; then + echo "PRNUM was already set to $PRNUM and is now being overridden with $1." + fi + PRNUM="$1" + shift + esac +done if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then echo "PR #${PRNUM} does not exist." @@ -14,7 +37,7 @@ fi SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?") git log master --grep "Merge PR #${PRNUM}" --format="%GG" -if [[ "${SIGNATURE_STATUS}" != "G" ]]; then +if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then echo read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r echo @@ -30,6 +53,14 @@ MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merg if git checkout -b "${BRANCH}"; then if ! git cherry-pick -x "${RANGE}"; then + if [[ "$NO_CONFLICTS" == "true" ]]; then + git status + echo "Conflicts! Aborting..." + git cherry-pick --abort + git checkout - + git branch -d "$BRANCH" + exit 1 + fi echo "Please fix the conflicts, then exit." bash while ! git cherry-pick --continue; do @@ -59,7 +90,7 @@ if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then fi fi -if [[ "${OPTION}" == "--stop-before-merging" ]]; then +if [[ "$STOP_BEFORE_MERGING" == "true" ]]; then exit 0 fi |