Thanks. I fixed it and pushed directly to master (since the PR was already merged, and this was a very minor fix)