[jbosstools-dev] [gitmigration] *dont* use the big green merge button on github.