Hello, quick question about using diff-filter in linux. In the scenario that in my repository, I first copy file1 to file2, then move file2 to file3 and delete file1, "git diff" returns: diff --git a/file1 b/file3 similarity index 100% rename from file1 rename to file3 but running "git diff --diff-filter=r" doesn't return anything. Only flag "t" will return the change. Can this be considered as a bug?