AdaCore / gnatcoverage

GNATcoverage: Coverage Analysis Tool
39 stars 9 forks source link

Issue #6 Building on RHEL-7 x86_64 plus ancillary cleanups #7

Closed okellogg closed 4 years ago

okellogg commented 4 years ago

Hello Olivier, I would like to make the changes to the commit messages that you propose. It seems that there is no "nice" way of doing this ? I would not like to use push --force. So, I guess I'll just throw away the existing fork and re-fork. Or do you know of an easier way of changing the pushed commit messages? Thanks.

pmderodat commented 4 years ago

Hello @okellogg,

The only way to edit the commit messages is to use --force. We don’t particularly consider that it’s bad: on the one hand, editting the history is completely fine in you local tree and your own fork (unlike the official master repository, nobody is supposed to base their work on these commits) and on the other hand keeping the commit history understandable has real value when doing archeology (for instance bisecting commits in order to find a regression).

In any case, removing a fork and re-creating seems to be much heavier (for you) and will get you to the same point as running git push -f… so better do the latter in my opinion. ;-)

Thank you again for your contribution,

claassistantio commented 4 years ago

CLA assistant check
All committers have signed the CLA.

okellogg commented 4 years ago

Hi @pmderodat,

Thanks for the advice which I now applied to my fork.

Cheers,

Oliver

pmderodat commented 4 years ago

Hello @okellogg,

It seems that there is a small git issue on your pull request, now: all commits to gnatcoverage we committed since you first opened your PR are applied on top of your changes (see https://github.com/AdaCore/gnatcoverage/pull/7/commits), making the PR drowned with changes that are already present in gnatcoverage (see https://github.com/AdaCore/gnatcoverage/pull/7/files). In order to make the history clean, I would advise to run:

git fetch git@github.com:AdaCore/gnatcoverage master
git rebase FETCH_HEAD
git push -f origin master

These commands will rebase your changes on top of the latest commits in our repository, and thus make the extra ones in your repository automatically go away.

I hope this helps,

okellogg commented 4 years ago

Hello @pmderodat,

Thanks for the hint which I just applied.

pmderodat commented 4 years ago

Great, thank you again! Your patches are not merged.

pmderodat commented 4 years ago

As a colleague noticed, I meant: “your patches are now merged”. :-)