You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
@lgoettgens added that on newer outdated pages like https://docs.oscar-system.org/v1.0/ the banner is already there. So it just remains to run DocumenterTools.OutdatedWarning.generate once per repository on the gh-pages branch
It remains for someone to tackle this -- perhaps @aaruni96 can have a look.
The text was updated successfully, but these errors were encountered:
I now added PRs to all of our repositories with the script changes, apart from Hecke. The script does not like the current Vitepress site there and is thus unable to determine the point in time when the warning was added already at release. This would need some more manual work.
Julia docs show a big red banner "This documentation is not for the latest version. Go to the latest documentation." on pages like https://docs.julialang.org/en/v1.7/
We should do the same for the OSCAR docs (and ideally also AA, Nemo, Hecke, etc.)
@thofma pointed out on Slack that JuliaDocs/Documenter.jl#1577 is relevant and that there is a script to add it to old documentation.
@lgoettgens added that on newer outdated pages like https://docs.oscar-system.org/v1.0/ the banner is already there. So it just remains to run
DocumenterTools.OutdatedWarning.generate
once per repository on thegh-pages
branchIt remains for someone to tackle this -- perhaps @aaruni96 can have a look.
The text was updated successfully, but these errors were encountered: