diff options
| author |  mlasson <marc.lasson@gmail.com> | 2015-06-25 16:40:24 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 00:46:52 +0200 |
| commit | 518049fe7f689489842fdfa670f57b618f125f31 (patch) | |
| tree | 9711507b00b03b120f12a2fb1c2d3f18d2d17d60 /library | |
| parent | 0f2d41755d99770c4576776462a4e433fb8f0a02 (diff) | |
Add an if_verbose for "Fetching opaque proofs ..."
I do not think that this information is worth displaying without
the verbose flag.
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml index 45fce1c26..f7ca4e976 100644 --- a/library/library.ml +++ b/library/library.ml @@ -379,7 +379,7 @@ let access_table what tables dp i = | Fetched t -> t | ToFetch f -> let dir_path = Names.DirPath.to_string dp in - msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); + Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path); let t = try fetch_delayed f with Faulty f -> |