Skip to content
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.

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

chore: remove old language manual #6401

Conversation

david-christiansen
Copy link
Contributor

To avoid user confusion, there should be just one manual.

This PR deletes the old manual, adding a link to the new one; the website config will redirect these pages to the corresponding new manual content.

To avoid user confusion, there should be just one manual. With the
release of the new one, the old content is all redirected to the
corresponding new sections' permalinks.
@david-christiansen david-christiansen added this pull request to the merge queue Dec 16, 2024
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 16, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0340f904b35ac90edef7e64bc81b53df7ecd7e14 --onto a8a160b09147c3225150703ac727eea6ee9a3b0e. (2024-12-16 14:39:12)

Merged via the queue into leanprover:master with commit 5fcd42d Dec 16, 2024
14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants