chore: Redirect case.html

[max-sixty]

This will fix the tests in #2040

[prql-bot]

The backport to web failed:

The process '/usr/bin/git' failed with exit code 1

To backport manually, run these commands in your terminal:

# Fetch latest updates from GitHub
git fetch
# Create a new working tree
git worktree add .worktrees/backport-web web
# Navigate to the new working tree
cd .worktrees/backport-web
# Create a new branch
git switch --create backport-2048-to-web
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 241d8933f5c50662055504fb4d2621f396d32200
# Push it to GitHub
git push --set-upstream origin backport-2048-to-web
# Go back to the original working tree
cd ../..
# Delete the working tree
git worktree remove .worktrees/backport-web

Then, create a pull request where the base branch is web and the compare/head branch is backport-2048-to-web.

[max-sixty]

Sorry, this was a terrible git mistake. I'm reverting the web branch and fixing.

[max-sixty]

OK I applied only the correct diff to web and pushed manually. It's correct that the redirect won't be on main, and so will get blasted away when we force push main when we release

[aljazerzen]

I git pinged from the commit message. Is using the backport bot really easier than a push to web branch?

[max-sixty]

I think you get pinged because it has every commit in it, because I messed up the merge.

Is using the backport bot really easier than a push to web branch?

Yes — much!