Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Already on GitHub? Sign in to your account

Bug 807841 - Use rm -r to delete directories. r=jmaher #43

merged 1 commit into from Nov 3, 2012


None yet
3 participants

wesj commented Nov 2, 2012

No description provided.

@wlach wlach added a commit that referenced this pull request Nov 3, 2012

@wlach wlach Merge pull request #43 from wesj/master
Bug 807841 - Use rm -r to delete directories. r=jmaher

@wlach wlach merged commit aabda91 into mozilla:master Nov 3, 2012

k0s commented Nov 4, 2012

Posting to https://bugzilla.mozilla.org/show_bug.cgi?id=807841 and mozilla#43 both for necessity and to illustrate a point.

As per https://wiki.mozilla.org/Auto-tools/Projects/MozBase#Working_on_Mozbase_and_Contributing_Patches the current status quo is to not use pull requests. One reason for this is that comments should be double posted in order that the issue can be followed coherently in both locations. If we want a different policy, we should consider a different policy. We should not subvert our own policy.

Is this issue closed or is it still active?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment