Skip to content

Conversation

capn-freako
Copy link
Contributor

At Matthew's request.

@capn-freako
Copy link
Contributor Author

capn-freako commented Jul 24, 2022

@MatthewDaggitt , why is this PR showing so many included commits?
There should only be one.
I pulled from upstream/master, after you accepted/merged PR #1767 ; I would've thought that doing so would prevent this sort of thing. Is there something else I need to do in addition?

The good news is: the actual file changes are exactly as I would expect.

@gallais
Copy link
Member

gallais commented Jul 25, 2022

You probably started your new PR from the branch already containing the commits instead of from master.
Pulling the updated master is not enough: you need to to checkout to it too.

Same for #1792

Edit: ah wait no it's because your own master is polluted by all of these commits: https://github.com/capn-freako/agda-stdlib
We have a guide on how to use git branches to avoid these issues.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants