[translations] how to remove a file

[Federico Bruni <fedelogy@xxxxxxxxx>]

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