diff options
| author | Pierre Boutillier | 2014-01-13 22:06:36 +0100 |
|---|---|---|
| committer | Pierre Boutillier | 2014-01-13 22:10:13 +0100 |
| commit | 679132dd7b193c5d19066696871ca13fafc35654 (patch) | |
| tree | 919aa9465f437f357f3a09eba3e04dd0075e60b9 /toplevel | |
| parent | e6b3b63eab1ca2a9586ef2c49a8df6c2e2a29adf (diff) | |
Make Require verbose
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 90d2029eaf..6ddde1e3d3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -716,7 +716,7 @@ let vernac_end_segment (_,id as lid) = let vernac_require import qidl = let qidl = List.map qualid_of_reference qidl in - let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in + let modrefl = List.map Library.try_locate_qualified_library qidl in if Dumpglob.dump () then List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl); Library.require_library_from_dirpath modrefl import |