diff options
| author | Enrico Tassi | 2019-08-02 14:08:17 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-08-02 14:08:17 +0200 |
| commit | e831ec5efd8b3b434eaf8b57b7150c3e8882e314 (patch) | |
| tree | f47a812423def7f3988da9df513d529bf327d54a /plugins/syntax | |
| parent | 12463d6d8064a79577efe0c231a768b3ef786cec (diff) | |
| parent | 845039dd1cab2066ca1ebc3cc09e726d21b1e671 (diff) | |
Merge PR #10543: Remove unused grammar nonterminals and productions
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions