diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh | 6 | ||||
| -rwxr-xr-x | dev/tools/make-changelog.sh | 3 |
2 files changed, 8 insertions, 1 deletions
diff --git a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh new file mode 100644 index 0000000000..f4840c2a83 --- /dev/null +++ b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10681" ] || [ "$CI_BRANCH" = "proof+private_entry" ]; then + + equations_CI_REF=proof+private_entry + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh index ea96de970a..ec59a6047f 100755 --- a/dev/tools/make-changelog.sh +++ b/dev/tools/make-changelog.sh @@ -7,7 +7,8 @@ echo "Where? (type a prefix)" (cd doc/changelog && ls -d */) read -r where -where=$(echo doc/changelog/"$where"*) +where="doc/changelog/$where" +if ! [ -d "$where" ]; then where=$(echo "$where"*); fi where="$where/$PR-$(git rev-parse --abbrev-ref HEAD).rst" # shellcheck disable=SC2016 |