[jdt-dev] Telling GitHub to rebuild, rebase, ...

[Stephan Herrmann <stephan.herrmann@xxxxxxxxx>]

It feels like I asked this before, but as I can't find this info in any 
canonical place I will keep asking:

How can I tell github to
- rebuild a PR unchanged
  (e.g., when a failure was intermittent, when a period check is outdated)
  - when a jenkins build is still available
  - after the jenkins build has been deleted
- rebase a PR on HEAD and rebuild

Please don't just answer here, but provide a link to the persistent, canonical 
location where such information can be found. Hopefully, that location can be 
remembered easily and will answer all related questions.

thanks,
Stephan

PS: Are there other tidbits committers should observe when working with github? 
In the bugzilla era there was a lot of information we recorded in each bug 
report, like Version and Target Milestone. Is JDT planning to apply similar 
discipline in github? Are labels to be used in some coordinated style?