On Wed, Jul 13, 2022 at 11:26 AM Daniel Shahaf <d...@daniel.shahaf.name> wrote: > > Daniel Shahaf wrote on Wed, 13 Jul 2022 14:54 +00:00: >> Incidentally, Daniel, r1902590 needs s/real'/realm'/.
Fixed, r1902705. Cheers, Nathan
On Wed, Jul 13, 2022 at 11:26 AM Daniel Shahaf <d...@daniel.shahaf.name> wrote: > > Daniel Shahaf wrote on Wed, 13 Jul 2022 14:54 +00:00: >> Incidentally, Daniel, r1902590 needs s/real'/realm'/.
Fixed, r1902705. Cheers, Nathan