On 05/11/20 03:37, Michael D Kinney wrote:

There was feedback from Laszlo related to rebase for
pull requests using the current CI process.

To clarify, I don't think we should allow any github-side automatism to
auto-rebase pull requests. I think such rebases need to occur on
personal developer machines, under human oversight, and then resubmitted
(likely: force-pushed). My request is that the build costs (time,
energy) associated with such force-pushes be reduced somehow.

For example, on a local machine, the following sequence:

$ git checkout master
$ git pull
$ git rebase -i master my_topic_branch
$ build ...

would trigger an incremental build. *.c files not touched by either
operation would not have to be re-built (assuming their dependencies
didn't change either, such as lib class headers, protocol headers, ...)

Thanks,
Laszlo