Stream: quantum computing

Topic: issue #11


view this post on Zulip Anthony Bordg (Jul 31 2019 at 19:02):

Some thought on that ?
@Yijun He @Hanna Lachnitt

view this post on Zulip Hanna Lachnitt (Jul 31 2019 at 19:15):

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.

view this post on Zulip Hanna Lachnitt (Jul 31 2019 at 19:18):

Or will this happen anyway when the file is renamed?
Edit: git mv old_filename new_filename preserves history and contributers

view this post on Zulip Anthony Bordg (Jul 31 2019 at 21:31):

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

view this post on Zulip Anthony Bordg (Aug 01 2019 at 08:57):

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.

view this post on Zulip Anthony Bordg (Aug 01 2019 at 11:22):

The master branch is now in its previous state.

view this post on Zulip Anthony Bordg (Aug 01 2019 at 11:25):

I used git mv to rename the theory MoreTensor.thy in the test branch. But, it reinitialised the list of contributors and history.

view this post on Zulip Anthony Bordg (Aug 01 2019 at 11:39):

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

view this post on Zulip Hanna Lachnitt (Aug 01 2019 at 12:33):

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?

view this post on Zulip Hanna Lachnitt (Aug 01 2019 at 12:35):

However, using git log --follow ./path/to/file is fine for me as well :)

view this post on Zulip Anthony Bordg (Aug 01 2019 at 14:09):

Issue closed on GitHub.

view this post on Zulip Hanna Lachnitt (Aug 01 2019 at 16:53):

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 :)

view this post on Zulip Hanna Lachnitt (Aug 01 2019 at 17:06):

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: Aug 15 2022 at 04:16 UTC