> > 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-mvReceived on Friday, 19 April 2013 08:44:28 UTC
This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 17:34:08 UTC