aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-05-31 22:22:08 +0000
committerGravatar vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-05-31 22:22:08 +0000
commit6b54af467dd9e4e26205e0f16e0c924240fadfe0 (patch)
treee75b7782701363820dc58df4fb4b9754be5372c1 /toplevel
parent509a55ed055a9d30e8c1501946a9bbeb19ecdbf3 (diff)
deporting Coq specific code from ide to toplevel.
Still messy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/toplevel.mllib1
2 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 32c597b2f..74c4ff3db 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -341,6 +341,7 @@ let init_toplevel = init
let init_ide arglist =
Flags.make_silent true;
Pfedit.set_undo (Some 5000);
+ Ide_blob.init_stdout ();
init arglist;
List.rev !ide_args
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 4c229d168..7443edefd 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -18,6 +18,7 @@ Mltop
Vernacentries
Whelp
Vernac
+Ide_blob
Toplevel
Usage
Coqinit