From 32ef206e99d7c186a33c470ae3c3af10519f80ac Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 16 Sep 2024 11:00:06 -0500 Subject: [PATCH] Test ssh-add --- .github/workflows/main.yml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 9e1b577..de18f6b 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -19,20 +19,18 @@ jobs: make github - name: Deploy tutorial on the cvc5 website - if: (github.repository == 'cvc5/tutorials') && (github.ref == 'refs/heads/main') - env: - SSH_AUTH_SOCK: /tmp/ssh_agent.sock + #if: (github.repository == 'cvc5/tutorials') && (github.ref == 'refs/heads/main') run: | - ssh-agent -a $SSH_AUTH_SOCK > /dev/null + eval $(ssh-agent -s) ssh-add - <<< "${{ secrets.CVC5_WEBSITE_TOKEN }}" git config --global user.email "cvc5-bot@users.noreply.github.com" git config --global user.name "cvc5-bot" git clone git@github.com:cvc5/cvc5.github.io.git website/ - rm -r website/tutorials/beginners - cp -r beginners/_build/html website/tutorials/beginners - cd website/ - git add tutorials/beginners - git commit -m "Deploy tutorials from source repo" - git push + # rm -r website/tutorials/beginners + # cp -r beginners/_build/html website/tutorials/beginners + # cd website/ + # git add tutorials/beginners + # git commit -m "Deploy tutorials from source repo" + # git push