| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Doc URLs may change with time because they depend on Doxygen machinery.
This is unfortunate because it is good practice to keep valid URLs
(see: https://www.w3.org/Provider/Style/URI.html).
I could not find a built-in solution in Doxygen, so the solution proposed
here is to maintain a registry of all URLs and manage legacy URLs as
redirections to their canonical page.
This commit adds a registry of URLs that has three functions:
- Check no previous URL is now invalid.
- Add aliases for moved pages.
- Generate redirection pages for aliases. The redirection works with
a simple <meta http-equiv="refresh"> HTML tag. See:
https://developer.mozilla.org/en-US/docs/Web/HTML/Element/meta#http-equiv
This commit also initialize the URLs registry with current pages and some
redirections needed after recent documentation refactoring.
Finally, the CI is updated to catch any change that invalidate previous
URLs.
|
| |
|
|
|
|
| |
Mostly to bump to macos one which will hopefully fix CI issues there.
Signed-off-by: Ran Benita <ran@unusedvar.com>
|
| |
|
|
|
|
| |
Node 12 is deprecated so let's bump the actions to newer versions that
use Node 16. See
https://github.blog/changelog/2022-09-22-github-actions-all-actions-will-begin-running-on-node16-instead-of-node12/
|
|
|
"main" is a bit non-descriptive, let's name them after the platforms we run them
on. Splitting them up allows us to be less selective on how we run the various
workflows, e.g. always running the linux one.
|
