diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-22 08:31:17 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-22 08:31:17 +0000 |
| commit | e19d39cc2796345d531b5a2d7dd33980f8989bfb (patch) | |
| tree | 39eb7137f514211bfccd30bb3e65a352bf72bbbd /pretyping | |
| parent | 9aa2464375c1515aa64df7dc910e2f324e34c82f (diff) | |
[printing] Remove duplicate definitions of pr_lident and pr_lname
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions