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@vger.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html