[Grace-core] Another Pull request

[Andrew P. Black]

Tim,

I just created commit 521630f1ed im my github repository, which is the changes to the naming conventions for collections that we decided on today.

However, desire your having walked me through the process of creating a pull request earlier, I cannot see how to create another pull request for this commit.

I also tried following the instructions here:  https://help.github.com/articles/creating-a-pull-request , which suggests creating a “compare” page (it don’t say why), and clicking the “create pull request” button on that page, but although I was able to create the compare page, there was such button on it.

I’m now wondering if it’s impossible for me to create a pull request until you have merged the previous one.   If this is true, it will be a problem.

	Andrew