Remove a file from PR

Stream: mathlib4

[Arien Malec]

What's the git-fu to remove lake-manifest.json from a PR?

I tried git checkout origin/master -- lake-manifest.json, then commit and push, but the changes are still in the PR...

[Yakov Pechersky]

Did you git add the modified/checked out file, before committing?

[Shreyas Srinivas]

git rm --cached ....

[Arien Malec]

Doesn’t that remove it from both?

[Arien Malec]

Actually that removes it from the index. But I just want upstream’s version and want to forget the (committed) changes it’s tracking.

[Shreyas Srinivas]

then you checkout the file from the preceding commit and add it and commit it

[Shreyas Srinivas]

git checkout <commit_id> <file_name>

[Shreyas Srinivas]

You presumably don't want the file to be tracked after that either. So applying git rm --cached will make sure that it is not tracked any further.

[Arien Malec]

Nope, now the PR wants to delete lake-manifest.json

[Arien Malec]

So here's the current situation:

the file change was tracked (inadvertently I think) when master was merged:

7584bce8 (HEAD -> port/Data.Seq.Computation, origin/port/Data.Seq.Computation) stop tracking lake-manifest.json
a069e055 removed modified lake-manifest from PR
3284f097 Merge remote-tracking branch 'origin/master' into port/Data.Seq.Computation

[Arien Malec]

now, I just rolled back to that commit...

7c416efe (HEAD -> port/Data.Seq.Computation, origin/port/Data.Seq.Computation) roll back lake-manifest
7584bce8 stop tracking lake-manifest.json
a069e055 removed modified lake-manifest from PR

[Arien Malec]

But what I really want to do is roll back the commit ID that modified it in the first place.

[Kevin Buzzard]

Why don't you just edit the file to what it is supposed to be and then push it? Is there a reason that you want to make it more complicated?

[Arien Malec]

It’s going to apply whatever is there when it merges. But yeah, once it’s approved someone with commit rights to master can checkout the latest then merge the PR and it will be a noop

[Yaël Dillies]

No it won't, right? We squash-merge PRs.

[Eric Wieser]

It would help a lot if you mentioned the relevant PR number so that we could actually see the git history you are talking about

[Arien Malec]

Mathlib4#1216

[Eric Wieser]

Is your comment there a note to self? Kevin's suggestion will work fine here; if you didn't intend to edit that file at all, then just replace its content with what master has and commit it.

[Arien Malec]

I did & the file was still there.

[Arien Malec]

That was the step in top of the thread.

[Arien Malec]

This change came along with the merge of master into this branch

[Arien Malec]

That’s why I think the solution here is to do that prior to merge.

[Shreyas Srinivas]

The simplest solution is @Kevin's. Checkout the file from an earlier version, add, and commit

[Shreyas Srinivas]

If you want an earlier version of the file