[Bug 543496] [pmi] Source repos and github repos section should be unified/merged

Bugzilla Link	543496
Status	NEW
Importance	P2 normal
Reported	Jan 16, 2019 06:45 EDT
Modified	Dec 15, 2020 15:56 EDT
See also	544376, 543455

Description

Unless there is a good reason to keep both sections separate, they should be merged into a single source repo section. It should not matter if a repo is hosted on git.eclipse.org or github.com/eclipse.
Sync tooling might need to be adapted accordingly.