>I haven't found navigating JIRA + GitHub PRs to be a significant >problem, but if others think it would help
GitHub has a single search field, so you can search for both PRs and issues at the same time which is nice as well. >will my GH comments end up as coming from @michaelmior If we migrate issues, then they will be created by a "bot" account. Of course, we can add comment author in the comment itself. Here's how Coq migrated their issues: https://github.com/coq/coq/issues/2268 We can figure out which accounts do we want to use (e.g. create email -> account mapping file). Vladimir
