+ [2015-04-01T21:15:13Z] jonfen_ is there any difference between creating a machine user on github and a regular user?
+ [2015-04-01T21:16:10Z] jonfen_ https://developer.github.com/guides/managing-deploy-keys/#machine-users
+ [2015-04-01T22:11:56Z] VxJasonxV not that they're here to get that answer

message no. 87581

Posted by sean_1 in #github at 2015-04-01T19:38:14Z

Does anyone know how to exclude "GoogleCodeExplorer" from a search?
+ [2015-04-02T00:39:51Z] ResidentBiscuit Can I get the same information through polling notifications that I can get from webhooks?
+ [2015-04-02T01:49:01Z] dodobrain can someone tell me what the workflow is on github for simple patches?
+ [2015-04-02T01:50:30Z] dodobrain i want to submit a pull request (patch) to a repository, do i simply fork the repo, make my changes, commit to my forked repo, submit a pull request and then delete my fork?
+ [2015-04-02T02:04:14Z] raz dodobrain: exactly