diff options
| author | Gaëtan Gilbert | 2018-05-01 13:21:48 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-01 16:17:50 +0200 |
| commit | a4ac6f904216ac28e70d9c0d03bff45960ba41a1 (patch) | |
| tree | 5edd8ae842cbe16a15afc09f92f0cc71376befba /kernel/type_errors.mli | |
| parent | 97ee8fbd0bf917c29e47f746c0a28623ebc7da9a (diff) | |
ci-vst.sh: use -o progs
This is closer to what we mean than reproducing the default target
without progs.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions