Skip to content

Merge branch 'develop' into feature_uncertainty #593

Merge branch 'develop' into feature_uncertainty

Merge branch 'develop' into feature_uncertainty #593

Workflow file for this run

name: mirror
on: [push, delete]
jobs:
mirror-to-CASUS:
runs-on: ubuntu-22.04
steps:
- uses: actions/checkout@v3
with:
fetch-depth: 0
- name: mirror-repository
uses: spyoungtech/[email protected]
with:
REMOTE: 'ssh://[email protected]/casus/mala.git'
GIT_SSH_PRIVATE_KEY: ${{ secrets.GIT_SSH_KEY }}
GIT_SSH_NO_VERIFY_HOST: "true"
DEBUG: "true"