extern/zrepl
1
0
Fork 0
mirror of https://github.com/zrepl/zrepl.git synced 2024-12-22 23:20:51 +01:00
Code Issues Actions Packages Projects Releases Wiki Activity

build: ci: fix quickcheck-docs for external PRs (#763)

Browse Source 
fixes https://github.com/zrepl/zrepl/issues/762
This commit is contained in:
Christian Schwarz 2023-11-01 00:12:23 +01:00 committed by GitHub
parent 21e0ae63a6
commit 30faaec26a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 20 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
.circleci/config.yml
View File

@ -58,6 +58,13 @@ commands:
git config --global user.email "zreplbot@cschwarz.com" git config --global user.email "zreplbot@cschwarz.com"
git config --global user.name "zrepl-github-io-ci" git config --global user.name "zrepl-github-io-ci"
# if we're pushing, we need to add the deploy key
# which is stored as "Additional SSH Keys" in the CircleCI project settings.
# We can't use the CircleCI-manage deploy key because we're pushing
# to a different repo than the one we're building.
- when:
condition: << parameters.push >>
steps:
# https://circleci.com/docs/2.0/add-ssh-key/#adding-multiple-keys-with-blank-hostnames # https://circleci.com/docs/2.0/add-ssh-key/#adding-multiple-keys-with-blank-hostnames
- run: ssh-add -D - run: ssh-add -D
# the default circleci ssh config only additional ssh keys for Host !github.com # the default circleci ssh config only additional ssh keys for Host !github.com