Learn more about these different git repos.
Other Git URLs
a32ed65
note to self: don't EVER delete state names Deleting the state name causes an old "state" value in a request file to be unrecognized by the newer version of the server, which is bad.