diff options
| author | Gaëtan Gilbert | 2019-01-17 18:47:46 +0000 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-17 18:47:46 +0000 |
| commit | b2877df2c79147bd2e26e53e43291b9b29a2aab8 (patch) | |
| tree | 5726b6595ef29361743b0af750f1c0524d2aa968 /pretyping | |
| parent | 47c6f0ddacf340d4027fce181ee8ac8a0369188f (diff) | |
| parent | 44b5f77f36011e797f0d7d36098296dc7d6c1c51 (diff) | |
Merge PR #9326: [ci] compile with -quick & validate after vio2vo
Reviewed-by: ejgallego
Ack-by: SkySkimmer
Ack-by: gares
Ack-by: ppedrot
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions