Closed MiguelCompany closed 3 years ago
Follow-up of #41
As git cherry-pick creates a commit, it requires git user configuration to be set.
This PR changes this for getting the diff of the commit with curl and using git apply with the downloaded diff.
curl
Signed-off-by: Miguel Company MiguelCompany@eprosima.com
Follow-up of #41
As git cherry-pick creates a commit, it requires git user configuration to be set.
This PR changes this for getting the diff of the commit with
curl
and using git apply with the downloaded diff.Signed-off-by: Miguel Company MiguelCompany@eprosima.com