diff options
| author | David Waern <david.waern@gmail.com> | 2008-10-20 20:25:50 +0000 |
|---|---|---|
| committer | David Waern <david.waern@gmail.com> | 2008-10-20 20:25:50 +0000 |
| commit | 7fc7a177035d450566c375e361ed0961c1d3fa0d (patch) | |
| tree | 051d7fa58c2f1522a1c91644c9d93676d6509db3 /examples | |
| parent | 5ddb372746432ff0e1026f62171c1e0e3a705a6f (diff) | |
Make renamer consistent
Instead of explicitly making some binders Undocumented, treat all names the
same way (that is, try to find a Documented name).
Diffstat (limited to 'examples')
0 files changed, 0 insertions, 0 deletions