diff options
| author | Emilio Jesus Gallego Arias | 2019-05-01 00:04:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-01 00:04:40 +0200 |
| commit | 213b5419136e4639f345e171c086b154c14aa62c (patch) | |
| tree | 893a5bbd7675427d0fae33c96d10159ceaf35b7a /dev | |
| parent | d6ebee1ad4b56d769227fab7373667eda3352fec (diff) | |
| parent | 708df3d3ebe5c6cf7c8b085beea986566fdab094 (diff) | |
Merge PR #10033: Remove the k0 argument from pretype functions.
Reviewed-by: herbelin
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions