diff options
| author | Emilio Jesus Gallego Arias | 2017-12-15 22:33:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-18 17:17:06 +0100 |
| commit | 43c46c5398704e78c609f9ee3a51d515f2746f0e (patch) | |
| tree | d1ab5c47b0c0985f8dd9e7406a2202483a1160ec /API | |
| parent | b6e05e2944c2a7976c4ac1f51694b175f52dbaf8 (diff) | |
[vernac] Cleanup of do_definition.
We remove a few old-style normalization and try to use the newer APIs,
however, it is hard to say whether the right magic is being used.
Diffstat (limited to 'API')
0 files changed, 0 insertions, 0 deletions