Skip to content

Conversation

@Folyd
Copy link
Member

@Folyd Folyd commented Aug 25, 2022

@notriddle
Copy link

  1. I definitely don't think you want to merge this until the new error index is stable.
  2. Even after the new error index is stable, there's a redirect in place so that the old URLs still work.

@Folyd
Copy link
Member Author

Folyd commented Sep 2, 2022

  1. I definitely don't think you want to merge this until the new error index is stable.
  2. Even after the new error index is stable, there's a redirect in place so that the old URLs still work.

Good to know, thanks @notriddle. 😸

@notriddle
Copy link

The new error index is stable. If you want to skip the redirect, this can merge now.

@Folyd
Copy link
Member Author

Folyd commented Feb 14, 2023

Merged. Thanks for reminding me. 😄 @notriddle

@Folyd Folyd deleted the error-index branch February 14, 2023 15:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants