Re: how to remove a file

[Federico Bruni]

I'm putting -devel in CC.
Sorry for pushing, I'm in a hurry: I'd like to send the patches within 
tonight.

Il 06/05/2012 15:53, Federico Bruni ha scritto:
> Hi,
>
> I have to remove the .texidoc file of a snippet which has been removed:
>
> diff --git
> a/Documentation/snippets/piano-template-with-centered-dynamics.ly
> b/Documentation/snippets/piano-template-with-centered-dynamics.ly
> deleted file mode 100644
> index f56fc58..0000000
> --- a/Documentation/snippets/piano-template-with-centered-dynamics.ly
> +++ /dev/null
>
>
> I wonder if I should use 'rm' or 'git rm'.
> I know that the difference is that rm keeps the file in the git index,
> while git rm removes it both from index and working copy.
> I think that I should use git rm, but I prefer asking as I have a poor
> understanding of git.
>
> Thanks,
> Federico

I made a try:

$ git rm 
Documentation/it/texidocs/piano-template-with-centered-dynamics.texidoc
error: 
'Documentation/it/texidocs/piano-template-with-centered-dynamics.texidoc' has 
local modifications
(use --cached to keep the file, or -f to force removal)

What's the recommended method?