Stream: quantum computing

Topic: issue #11

Anthony Bordg (Jul 31 2019 at 19:02):

Some thought on that ?
@Yijun He @Hanna Lachnitt

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.

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

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

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.

Anthony Bordg (Aug 01 2019 at 11:22):

The master branch is now in its previous state.

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.

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

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?

Hanna Lachnitt (Aug 01 2019 at 12:35):

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

Anthony Bordg (Aug 01 2019 at 14:09):

Issue closed on GitHub.

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

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

• create a new branch (actually make it two new branches for data loss prevention)
• In the master branch follow the instructions of the first answer here: https://stackoverflow.com/questions/42332769/how-do-i-reset-the-git-master-branch-to-the-upstream-branch-in-a-forked-reposito
• Go to the new branch and checkout all the stub files, leave only the ones that you made changes to.
• Do a pull request to the branch (create or update it) you want to have your files in

I am not sure as this works for anyone as there was another fork-specific problem at my fork.

Last updated: Apr 20 2024 at 08:16 UTC