Re: #5355 Doc: document grob metadata in SVG output in Notation Reference

[David Kastrup]

"James Lowe" <address@hidden> writes:

> Hello
>
> On Sun, 1 Jul 2018 09:59:11 +0200, Urs Liska <address@hidden> wrote:
>
>> 
>> 
>> Am 01.07.2018 um 09:55 schrieb James Lowe:
>> > I don't know what the difference is between pull and fetch in
>> > terms of 'rights' but I'd have thought it would be the same right?
>> >
>> 
>> Yes, the difference comes only on your own computer.
>
> Which has not changed (in terms of ssh keys, ./gitconfig etc.) for about 2 
> years.
>
> and like I said, it worked again briefly between about 11am and 3pm yesterday.
>
> Can someone else try to fetch?

I've had several Patchy-staging runs yesterday (for testing purposes)
where fetching failed, either at the start or at the end.  Manually
calling fetch tended to work.  So it was intermittent.  I found it weird
but ascribed it to my network connection (though I had no other problems
with it at the time).  Right now fetch works.

-- 
David Kastrup