diff options
| author |  vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-14 14:43:01 +0000 |
|---|---|---|
| committer | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-14 14:43:01 +0000 |
| commit | c9a9752c76bfb592d775a7fdb9ebe4702ff1aaef (patch) | |
| tree | 10bf7c57d0ae1c66481d1ea72a4dd438ebc5525e /toplevel/coqtop.mli | |
| parent | 4b6b6ba87ee19854bb8464cb248fcf40f0b965e1 (diff) | |
CoqIDE argv parsing delegated to coqtop
Introduces some hacks to have a consistent user experience. When coqtop
prints info on self then exit, return code is 2 if called with
-filteropts, 0 else
For now, no options are accepted by coqide. there is no way for now to
specify a filename that begins with a dash.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/coqtop.mli')
| -rw-r--r-- | toplevel/coqtop.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 2c55f6509..9da66398c 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -12,10 +12,3 @@ produce the output state if any, and finally will launch [Toplevel.loop]. *) val start : unit -> unit - -(** [init_ide] is to be used by the Coq IDE. - It does everything [start] does, except launching the toplevel loop. - It returns the list of Coq files given on the command line. *) - -val init_ide : System.physical_path list -> string list - |