Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Redis fixes #637
Thank you! Merging in now.
You can update the pull request by modifying the history of the original branch, for example by using an interactive git rebase and re-authoring the affected commit. If you then