When a PR is opened on Github, cross-reference on Gitlab
Example:
- A pull-request is opened on Github, with a reference to
dev/core#123
in the title
- A bot should update the Gitlab issue so that people are informed, and can easily navigate from one to the other.
related to #3
Edited by bgm