With github pullrequests work on target repo rather than the source#816

Open

timor-raiman wants to merge 1 commit intoros-tooling:masterfrom timor-raiman:master

+10-4

Commits on Apr 20, 2023

Working with pullrequests, must stick to target repo consistently
timor-raiman
committed