Thanks for all the replies!
Now I see pretty clear; a quick summary
(in case somebody else wants to learn from this):
1.
"git mv file new_file" seems to be (exactly?) equivalent to
mv file new_file
git rm file
git add new_file
(Perhaps this information could be added to the git-mv-documentation?
I would have found it useful (since I had a different expectation).)
2. To do something with the history, for example to rename "file"
to "new_file" also in the whole history, a new repository (or
a new branch) has to be created. Three possibilities:
(a) Using the basic git-functionality, re-creating a repository
by re-creating all commits (with appropriate changes) by "hand"
or "script".
(b) More convenient, the upcoming "git-filter-branch" apparently
makes filtering out easier.
(c) Or, apparently more powerful, with "cg-admin-rewritehis"
(part of the cogito-tool) we have quite a powerful tool
for creating a branch with a (re-created and modified)
history (the documentation explicitely mentions how to
remove a file from history --- that is, in the new branch).
Hope that's correct.
Thanks a lot to all!
Oliver
-
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
