diff options
| author | Hugo Herbelin | 2016-07-17 09:22:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-17 10:45:27 +0200 |
| commit | 152aca663d76f0cfda21ddef880050f21bfe4995 (patch) | |
| tree | 7d2bf7549f1e068aa38b4ecfd80c8677936cd0ab /plugins | |
| parent | d17237cfd3a67b9a93de98a23ae29869456d2028 (diff) | |
Fixing a bug in recognizing a recursive pattern of notations
immediately in the scope of another recursive pattern.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions