diff options
| author | Pierre-Marie Pédrot | 2016-08-29 12:22:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-29 14:05:40 +0200 |
| commit | 95212aba8ba0ad76e6ee913566040f5c6e2c291d (patch) | |
| tree | 096644b642082128eb0fa1c72be9fd64975b1a83 /Makefile.dev | |
| parent | aa0ad1713b109da690f9a56358df1f5ba56c65e6 (diff) | |
Fix tagging of notations.
We only tag the non-whitespace substrings, rather than the whole terminal token.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions