diff options
| author | Gaëtan Gilbert | 2020-12-16 10:22:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-12-16 10:25:55 +0100 |
| commit | faafe8bfb97e7b05afbcc903cc946d9fca038df5 (patch) | |
| tree | 34ffdd5643de382ebc2f597abff09ff7732c20d7 /kernel/type_errors.mli | |
| parent | 46c55ced3d1a78f63b3b50fc12d9760663e87e57 (diff) | |
Fix overlay system: projects need to be loaded before overlays.
Also fixes is_in_projects
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions