aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2012-09-07 16:55:28 +0000
committerletouzey2012-09-07 16:55:28 +0000
commitba59073c997a22a30676b4e900a732fc2ba03da2 (patch)
tree92f8bf8fa69bb3882149b8afe357197ee8db5e91
parent882e9d8f03d7b40c850f04d3f33a32950035244a (diff)
Avoid [Loading ML file ...] messages when launching coqtop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15783 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--toplevel/coqtop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a5673578f5..a97d8748a6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -106,7 +106,7 @@ let require_prelude () =
let require_list = ref ([] : string list)
let add_require s = require_list := s :: !require_list
let require () =
- if !load_init then require_prelude ();
+ if !load_init then silently require_prelude ();
List.iter (fun s -> Library.require_library_from_file None s (Some false))
(List.rev !require_list)