.github: Rename workflows for clarity

This commit is contained in:
Zhaofeng Li 2022-01-02 13:15:41 -08:00
parent f9fab83030
commit 1adb0b4246
2 changed files with 2 additions and 2 deletions

View file

@ -2,7 +2,7 @@
# the next stable release. For the one that is currently in
# effect, check the release branches (e.g., release-0.2.x).
name: Manual (Stable)
name: Deploy Stable Manual
on:
push:

View file

@ -1,4 +1,4 @@
name: Manual
name: Deploy Unstable Manual
on:
workflow_run: