please dont push to the records-and-sealed repo

[Vicente Romero]

I have created a new branch named: `records` that should from now on 
contain all the code for records. The former records-and-sealed will 
still be open for a while for reference etc but please push any new code 
for records into the new branch,

Thanks,
Vicente

On 10/15/19 10:34 PM, Vicente Romero wrote:
> Hi,
>
> I'm extracting the record bits from the records-and-sealed types to 
> create an independent repo, please don't push any record related code 
> until the new repo is available,
>
> Thanks,
> Vicente