Closed dreispt closed 3 months ago
Mmmmh, a force push is not wanted. @sbidoul Any advice ?
Doing this, there's a diff of 60 MB instead of 30. A forced push should be done instead for removing this cleanly.
FWIW:
❯ du -h .git --max-depth=0 50M .git ❯ git rm *.deb ❯ git commit -m "remove .deb file" ❯ du -h .git --max-depth=0 50M .git
So IMHO, this PR is better than the status quo.
I did the same experiment in a fork, and once pushed seems to be the problem. But anyway, I'm going to do the cleanup this week as said, previously announcing it in the contributors list.
But anyway, I'm going to do the cleanup this week as said, previously announcing it in the contributors list.
@pedrobaeza I think we need more evidence that this is worthwhile before doing such a disruptive operation.
Even if the removal doesn't add size, the inclusion of deb files does, so it must be cleaned.
Even if the removal doesn't add size, the inclusion of deb files does, so it must be cleaned.
Well, must is a big word and the tradeoffs are not that all obvious to me. Please make sure to provide data and gather consensus on the contributors mailing list before doing any force push.
Yes, because we are wasting a lot of resources. The trade-offs are very little and have direct mitigation actions. That's why I'm so categorical.
Doing this, there's a diff of 60 MB instead of 30. A forced push should be done instead for removing this cleanly.