From dfbfa6d133e979afa70806072ec128fd9e291ed9 Mon Sep 17 00:00:00 2001 From: Mitja Devetak Date: Mon, 22 Jan 2024 17:46:12 +0100 Subject: [PATCH] website --- .github/workflows/deploy_docs.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/deploy_docs.yml b/.github/workflows/deploy_docs.yml index 4f28ee2..6d7dc20 100644 --- a/.github/workflows/deploy_docs.yml +++ b/.github/workflows/deploy_docs.yml @@ -19,7 +19,8 @@ jobs: julia --project=docs/ -e 'using Pkg; Pkg.develop(path=pwd()); Pkg.add("Documenter"); Pkg.instantiate()' - name: Build and deploy env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + MY_GITHUB_TOKEN: ${{ secrets.MY_GITHUB_TOKEN }} + run: | julia --project=docs/ docs/make.jl cp -r docs/build/* docs/ @@ -29,5 +30,5 @@ jobs: git config --local user.name "GitHub Action" git add docs/ git commit -m "Update documentation" -a || echo "No changes to commit" - git push + git push --force https://${{ secrets.MY_GITHUB_TOKEN }}@github.com/Devetak/DiscoDiff.jl.git