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
don't not add duplicated references #3107
HACK: workaround for #2811
For my part I'd say this change (if we want to do it) needs to go to a different place.
Edit: TO clarify the "different" place is probably
Just some notes on this:
Yeah, I don't like this "solution" either.