please dont push to the records-and-sealed repo

[Vicente Romero]

done, now any new sealed code should go to: records-and-sealed,

Thanks,
Vicente

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