- From: Tobie Langel <tobie@w3.org>
- Date: Fri, 19 Apr 2013 10:44:19 +0200
- To: Robin Berjon <robin@w3.org>
- Cc: Peter Linss <peter.linss@hp.com>, Michael[tm] Smith <mike@w3.org>, public-test-infra <public-test-infra@w3.org>
> > On Wednesday, April 17, 2013 at 10:42 AM, Robin Berjon wrote: > > > Also, I *think* that git is smart enough to notice that something > > > was moved and merge properly. > > > So I ran a small scale experiment[1] and what happens is that current pull requests continue to be made against the original directory name, not the new one, and so merging the PR creates a new directory with the previous name. I suggest we still go ahead with this and either: 1) get folks to update their PRs, or 2) merge them as is and just mv the files to the new directory after the merge. Thoughts? --tobie --- [1]: https://github.com/tobie/test-pr-after-dir-mv
Received on Friday, 19 April 2013 08:44:28 UTC