(original) (raw)

If you create a dev branch that is going to live for less than 24 hours because you edited some typo in the docs or something through GitHub's UI, then that's fine. But long-lived dev branches should be done in one's personal fork. This is for two reasons: one is so that others don't inadvertently download your dev branch when they do a \`git pull\` (and because people often forget to do \`git pull --prune\`), and two because it eats up our CI (which is especially precious while we are still on AppVeyor and the turn-around time there is so long).