Skip to content

Remove "Edit this page on GitHub" from outdated doc pages #13355

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
bishabosha opened this issue Aug 23, 2021 · 2 comments · Fixed by #13359
Closed

Remove "Edit this page on GitHub" from outdated doc pages #13355

bishabosha opened this issue Aug 23, 2021 · 2 comments · Fixed by #13359
Labels
area:doctool

Comments

@bishabosha
Copy link
Member

from this comment: #13327 (comment)

leaving the "Edit this page on GitHub" link on the docs, e.g. at https://dotty.epfl.ch/docs/reference/other-new-features/export.html will lead to more PR's being generated here
@bishabosha bishabosha mentioned this issue Aug 23, 2021
Closed
@BarkingBad
Copy link
Contributor

BarkingBad commented Aug 23, 2021 •
edited
Loading

I don't know if this will be valid after merging #13350 because we will not generate static docs anymore, just preprocess the subset of them for docs.scala-lang website

@dwijnand dwijnand linked a pull request Aug 23, 2021 that will close this issue
Remove "Edit this page on GitHub" #13359
Merged
@julienrf
Copy link
Contributor

We need this before we can merge #13350

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
area:doctool
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Remove "Edit this page on GitHub" scala/scala3
3 participants
@julienrf @bishabosha @BarkingBad