please dont push to the records-and-sealed repo

[Vicente Romero]

I will put the old records-and-sealed branch to depend on the new 
records branch, please don't push just yet till I have done that merge,

Thanks,
Vicente


On 10/16/19 5:08 PM, Vicente Romero wrote:
> 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
>