On 19/04/2013 10:44 , Tobie Langel wrote: > 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. Rats. > 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. That works for me. In order to avoid problems, maybe whoever makes the renaming would have the kindness of going through the PRs to check? I'm happy to divvy up the work for this, e.g. by listing the name changes to be made in an Etherpad and going through them. -- Robin Berjon - http://berjon.com/ - @robinberjonReceived on Friday, 19 April 2013 08:50:25 UTC
This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 17:34:08 UTC