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 /Makefile.dev | |
| 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 'Makefile.dev')
| -rw-r--r-- | Makefile.dev | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev index 9659f602d7..13b85dfad4 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -63,7 +63,7 @@ revision: coqlight: theories-light tools coqbinaries -states: theories/Init/Prelude.vo +states: theories/Init/Prelude.$(VO) miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte |