Some thought on that ?
@Yijun He @Hanna Lachnitt
First of all, thanks @Josh Chen for writing the ROOT file. Right now the history of More_Tensor does only contain one single entry that is the renaming of the name of the theory. This is pretty confusing thus I would vote for changing it back.
Or will this happen anyway when the file is renamed?
Edit: git mv old_filename new_filename
preserves history and contributers
The correct way to do it is git revert -m 1 32d534ebf35eae7027e4f6e5ccb740d231dd25d2
, no ? Then use the command suggested by Hanna to preserve history and contributors of the theory MoreTensor.thy
.
@Yijun He @Hanna Lachnitt
I got Reverting is not possible because you have unmerged files. Ok, I used successfully git reset --hard <commit>
on a branch test. I should now try to do the same on the master branch.
The master branch is now in its previous state.
I used git mv
to rename the theory MoreTensor.thy
in the test branch. But, it reinitialised the list of contributors and history.
As it happens, there is no satisfying way to rename a file with Git while keeping the history and the list of contributors. It appears that it's an intentional design choice of Linus Torvalds.
However, one can keep track of history through renaming using git log --follow ./path/to/file
.
@Yijun He @Hanna Lachnitt
It was for a long time but it should be possible now see e.g.
https://koukia.ca/rename-or-move-files-in-git-e7259bf5a0b7
https://help.github.com/en/articles/renaming-a-file-using-the-command-line
https://stackoverflow.com/questions/2314652/is-it-possible-to-move-rename-files-in-git-and-maintain-their-history
Did you left everything untouched except for the file name?
However, using git log --follow ./path/to/file
is fine for me as well :)
Issue closed on GitHub.
I fixed the problem I had with git, I will write a short guide in case @Yijun He gets the same problem. All thanks go to Nathanael, without him I would have been lost :)
Okay so here is what you could try to avoid having several files in your pull request that you actually never changed (and that are actually unchanged but git does not recognize it).
I am not sure as this works for anyone as there was another fork-specific problem at my fork.
Last updated: Oct 13 2024 at 01:36 UTC