mirror of
https://github.com/postgres/pgweb.git
synced 2025-08-01 15:54:53 +00:00
e2120f0a80
The web documentation used to suffer from a problem that if a documentation page were renamed in a newer version, any references pointing to said documentation would be lost. For example, the feature known as "Default Roles" was renamed to "Privileged Roles" but caused a change in the URL. This patch introduces the ability to create a "DocPageRedirect" by specifying the previous name of the documentation page (e.g. "default-roles.html") and the new name (e.g. "privileged-roles.html") such that the continuity is preserved between versions.