+ [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. 87548

Posted by Lirux in #github at 2015-04-01T09:59:15Z

What is the best way of managing dotfiles of desktop and laptop which differ a little (font sizes, shortcuts etc..)? Branch for every machine?
+ [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