doc: rename file (#9208)

This commit is contained in:
Sylvestre Ledru
2025-11-09 22:54:08 +01:00
committed by GitHub
parent bfd0cfa195
commit f277e4e038