diff options
| author | Théo Zimmermann | 2019-03-10 23:32:23 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-10 23:32:23 +0100 |
| commit | 200a1712b9948fa7682dc95eeb0a520d6804caaf (patch) | |
| tree | 0d8b1dbe636fb87e6fbc5e238083729da469db0a /kernel/type_errors.ml | |
| parent | 51e88f1f19cc5c817773ff7be09f1b36008c8e17 (diff) | |
| parent | f5ac4945006ddd0924331bd956b6a25a6e5cc21f (diff) | |
Merge PR #9728: Fix issue #9722 pkg-config not found
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions