Skip to content

Add user name and host name to user-specific file directory #243

Add user name and host name to user-specific file directory

Add user name and host name to user-specific file directory #243

Workflow file for this run

name: Auto Merge
on: [pull_request_target, workflow_dispatch]
permissions:
contents: write
pull-requests: write
jobs:
automerge:
runs-on: ubuntu-latest
# Run only if PR is inside JabRef's main repository and created by dependabot or by an update workflow
if: >
(github.repository == 'JabRef/jabref') &&
((github.actor == 'dependabot[bot]') ||
((startsWith(github.event.pull_request.title, '[Bot] ') || (startsWith(github.event.pull_request.title, 'Bump '))) &&
(github.event.pull_request.head.repo.full_name == 'JabRef/jabref')))
steps:
- name: Approve PR
run: gh pr review --approve "$PR_URL"
env:
PR_URL: ${{github.event.pull_request.html_url}}
GITHUB_TOKEN: ${{secrets.GH_TOKEN_JABREF_MACHINE_PR_APPROVE}}
- name: Merge PR
run: gh pr merge --auto "$PR_URL"
env:
PR_URL: ${{github.event.pull_request.html_url}}
GITHUB_TOKEN: ${{secrets.GITHUB_TOKEN}}