[git] Correctly call git ls-tree so unicode files are not quoted#3879
Merged
nojb merged 2 commits intoocaml:masterfrom ejgallego:git+fix_ls_treeOct 23, 2020
+111-5
git ls-tree so unicode files are not quoted#3879