Age | Commit message (Collapse) | Author |
|
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.
|
|
|
|
This allows us to say that "app-pgreceivexlog.html" is actually the same
as "app-pgreceivewal.html" on a different version.
Turns out the templates would already render this correctly if we could
just find the map, so it's a simple case of adding an additional join
(that the django orm can't figure out, but we can do it in manual sql).
Adds a non-django managed unique index to make sure that it's not
possible to add the same alias twice in different "directions".
Violating this will cause a django excpetion in the admin interface
since it doesn't know about it, but as this is a very uncommon operation
and admin only, we don't care about that.
Finally, we don't bother issuing varnish purges for changes here, the
admin is expected to handle those manually. These changes are supposed
to happen very seldom, and the contents are purged automatically when
the docs are loaded anyway.
|
|
Per discussion from a long time ago, interactive docs aren't really
working out. The majority of submissions are either support questions
(which then get rejected because they cannot be answered in this
context) or pointing out docs incorrectnesses (which should be submitted
as a docs bug instead, so they can actually be fixed in the main
documentation).
Old references to /interactive/ will get redirected to /static/
automatically, and we expect to keep doing that for a long time (since
there are many links to them around the net).
|
|
|
|
|
|
|
|
|