name: 'Push directory to another repository' description: 'Useful to push files to another repository to be used, for example, via github pages' inputs: source-directory: description: 'Source directory from the origin directory' required: true destination-github-username: description: 'Name of the destination username/organization' required: true destination-repository-name: description: 'Destination repository' required: true user-email: description: 'Email for the git commit' required: true user-name: description: '[Optional] Name for the git commit. Defaults to the destination username/organization name' required: false default: '' destination-repository-username: description: '[Optional] Username/organization for the destination repository' required: false default: '' target-branch: description: '[Optional] set target branch name for the destination repository. Defaults to "master" for historical reasons' default: 'master' required: false commit-message: description: '[Optional] commit message for the output repository. ORIGIN_COMMIT is replaced by the URL@commit in the origin repo' default: 'Update from ORIGIN_COMMIT' required: false github-server: description: 'Github server' default: 'github.com' required: true runs: using: 'docker' image: 'Dockerfile' args: - ${{ inputs.source-directory }} - ${{ inputs.destination-github-username }} - ${{ inputs.destination-repository-name }} - ${{ inputs.user-email }} - ${{ inputs.user-name }} - ${{ inputs.destination-repository-username }} - ${{ inputs.target-branch }} - ${{ inputs.commit-message }} - ${{ inputs.github-server }} branding: icon: 'git-commit' color: 'green'