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
Fix include tag to avoid NameError #1494
I probably could, but what for? It's a valid suggestion worth of discussion, you already have a PR ready, and it might be best to let them be separate, so each one can be discussed and merged or rejected independent from the other. They shouldn't even conflict.
Here it is: