diff options
| author | Emilio Jesus Gallego Arias | 2018-08-28 13:06:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-08-28 13:06:38 +0200 |
| commit | a57891211e578605f6cb7e05f5fdadd7de49e519 (patch) | |
| tree | 6d0ff373cfd3ae87f226cef1909864647cb1dcab /kernel/type_errors.ml | |
| parent | f885e8a88620351d9dc4b0969f520d13197f2184 (diff) | |
| parent | aafe0040d6b4a69b4a6093a3262473e675387664 (diff) | |
Merge PR #8333: Fix URIs in the configuration script
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions