diff options
| author | Hugo Herbelin | 2016-04-16 13:03:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:48 +0200 |
| commit | 043d6a5c113a11fe9955cbe71b8f4bcd08af9a90 (patch) | |
| tree | a5fc1da04f6160f45b7f1c1e80458ab2b5ea5abb /plugins/syntax | |
| parent | 90252e973f5bcafc5f3b0b18564612d7fb4503a8 (diff) | |
Taking into account the original grammar rule to print generic
arguments of vernac extensions, so that in list with a separator, the
separator is printed.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions