Stream: Coq devs & plugin devs

Topic: Grammar not current


view this post on Zulip Notification Bot (Dec 06 2022 at 10:11):

Maxime Dénès has marked this topic as unresolved.

view this post on Zulip Maxime Dénès (Dec 06 2022 at 10:11):

Unfortunately, on one of them, I now get:

Error: doc/sphinx/user-extensions/syntax-extensions.rst line 33: MULTIPLE MATCHES for `Notation @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @scope_name }`
    Please update the rst manually while preserving any subscripts, e.g. 'NT__sub'

What does it mean?

view this post on Zulip Théo Zimmermann (Dec 07 2022 at 08:48):

Maxime Dénès said:

Thanks a lot! I wonder why the error message doesn't say it. Probably so that we get an occasion to chat.

The PR template tells you what to do though, but I've observed how old-timer never read the PR template, because they think they already know the information it contains.

view this post on Zulip Karl Palmskog (Dec 07 2022 at 10:14):

as a very occasional PR submitter, I think the "new" PR templates are great, very informative and link-y.


Last updated: Feb 05 2023 at 20:03 UTC