Learn more about these different git repos.
Other Git URLs
7f8273d
MAN: clarify which shell option takes precedence