+ [2020-06-03T18:48:09Z] SirCodesAlot jhass: that looks relevant to me?
+ [2020-06-03T18:48:59Z] SirCodesAlot thx.. I just signed up for the beta.. I'm doing some silly research for work, and these results would be helpful
+ [2020-06-03T19:13:40Z] Intelo I use github pro. Github teams is same price now. Is the latter better? I can see from features but asking you guys due
+ [2020-06-03T19:13:42Z] Intelo │ | to your experience?y

message no. 181751

Posted by chris11 in #github at 2020-06-03T18:00:53Z

or it could just run on every file committed, and show a warning instead of blocking the merge.
+ [2020-06-04T08:54:14Z] neper_romain I have a project with multiple GitHub repositories, namely one development (private) repo, share with a few teammates, and one public repo. How can I manage issues on both repos? since they will be assigned the same numbers (they always start from 1). Is it possible to reference issues, pull requests, etc. more accurately than by only their numbers?
+ [2020-06-04T09:11:10Z] jhass Github generally prettyfies full internal URLs, so https://github.com/org/repo/issues/1 will be rendered as #1 inside repo and org/repo#1 outside it. There might be some support for parsing the second style into a link, I never tried
+ [2020-06-04T09:17:39Z] nedbat neper_romain: your "one development (private) repo and one public repo" makes it sound like the two repos are the same code? As if you keep the code private until it is ready and then you make it public?
+ [2020-06-04T09:21:37Z] nedbat neper_romain: thee easiest thing would be to only have the public repo. Why keep the code secret and then make it public?