Add more granular tags to label documentation PRs

For #4285.
This commit is contained in:
Antonin Delpeuch 2021-11-09 09:45:13 +01:00 committed by GitHub
parent c22000a9a2
commit a983781bf7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -1 +1,3 @@
documentation: ["/docs"]
"current docs": ["/docs/docs"]
"historical docs": ["/docs/versioned_docs"]