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