+ [2016-11-21T20:28:32Z] Dougie187 Maybe it'll show up in both cases.
+ [2016-11-21T20:28:39Z] Dougie187 I don't know why it would be different in either case for that.
+ [2016-11-21T20:28:46Z] Dougie187 I'd guess it just takes some time for the server to analyze all of it?
+ [2016-11-21T20:30:01Z] disi maybe... tho the one that isnt showing up was configured first
+ [2016-11-21T21:23:49Z] disi this seems particularly relevant https://stackoverflow.com/questions/11370239/creating-an-official-github-mirror

message no. 157227

Posted by disi in #github at 2016-11-21T20:14:44Z

ok, now im confused. the point of mirroring would be to automatically receive new commits from the real github
+ [2016-11-22T00:03:24Z] bderrly is it possible to change the head branch of a pull request or do i need to close the request and open a new one?
+ [2016-11-22T00:51:15Z] kspencer for webhooks, how would one get the user that starred the repo
+ [2016-11-22T00:52:15Z] kspencer in the api sense
+ [2016-11-22T03:29:57Z] gmn8719 I submitted a pull request and it was accepted. It was suggested that I could delete my branch. Do they mean on the fork I created? If so, should I also update the fork as well? If so, how do I do that?
+ [2016-11-22T10:38:10Z] xall i want to add a log file to reference in a pr request i'm submitting. when i try to add a .log file, github errors saying it only accepts filetypes blahblah. what's the proper way to do this?