diff options
| author | Gaëtan Gilbert | 2020-04-20 23:16:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-20 23:16:42 +0200 |
| commit | f6f789f577efec5cfcd16c98290dab81162aa64c (patch) | |
| tree | 817382b17554f7106e38b5083d2e5936419eae35 /kernel/type_errors.mli | |
| parent | 51a938a260d989f11fb1cd1d7a0205c6183f3809 (diff) | |
| parent | 9849b21d756f2603e57363124be83bd87ff33af6 (diff) | |
Merge PR #12126: TIMEFMT: Display the output file name
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions