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 /checker | |
| 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 'checker')
| -rw-r--r-- | checker/check.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/check.ml b/checker/check.ml index 30437e8bd0..b2930d9535 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -329,7 +329,7 @@ let intern_from_file (dir, f) = user_err ~hdr:"intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin - chk_pp (str " (was a vio file) "); + Flags.if_verbose chk_pp (str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) |