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: