Fix name of documentation scripts (#80)

This commit is contained in:
Robert Luke 2021-08-11 19:54:15 +10:00 committed by GitHub
parent 8a3b0d2a8a
commit 7799ea1749
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -1,4 +1,4 @@
name: permanent
name: Build documentation
on:
push:
branches:
@ -13,4 +13,4 @@ jobs:
version: '1.6'
- uses: julia-actions/julia-docdeploy@releases/v1
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}