Le 24/02/2020 à 17:33, Christopher Schultz a écrit : > Any ideas?
I guess you are cherry picking the merge commit, instead of the actual commit(s) from the PR branch. Emmanuel Bourg --------------------------------------------------------------------- To unsubscribe, e-mail: [email protected] For additional commands, e-mail: [email protected]
