aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-11-08 12:32:55 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-11-08 12:32:55 +0000
commitafe0053676782fa7c990af622e95924d6ce5aaf7 (patch)
treed42dc674c3f96c63f5591d6d29b55863f9891243 /toplevel
parent9cd50d8f1be42e32cc82fb4bd0d2ead4ed55e1f7 (diff)
Choucroute entre les tables de synchronisation, les options -silent et les etats initiaux de coq. Pour l'instant je remets Silent en asynchrone.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2169 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8ccdd3976..6fd7f8858 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -779,7 +779,7 @@ let _ =
| _ -> bad_vernac_args "PrintSec")
let _ = declare_bool_option
- {optsync = true;
+ {optsync = false;
optname = "silent";
optkey = (PrimaryTable "Silent");
optread = is_silent;