diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-12 16:27:19 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-12 16:27:19 +0000 |
| commit | 62b92230d3ed0c01ce6cdb7bc59635ca7f659a9c (patch) | |
| tree | f9e9b1da8d0f9b387ab8f80bf58f4e530f553e5d /scripts | |
| parent | 0c0c605756d4c1f05b8ddf0d9ff7ad2f4926772a (diff) | |
remove old traces of SearchIsos (never ported to 7.x nor 8.x)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13986 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqmktop.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 0ff487fb4..14f26582f 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -49,7 +49,6 @@ let notopobjs = gramobjs let opt = ref false let full = ref false let top = ref false -let searchisos = ref false let echo = ref false let src_dirs () = @@ -133,7 +132,6 @@ let usage () = \n -echo Print calls to external commands\ \n -full Link high level tactics\ \n -opt Compile in native code\ -\n -searchisos Build a toplevel for SearchIsos\ \n -top Build Coq on a OCaml toplevel (incompatible with -opt)\ \n -R dir Specify recursively directories for Ocaml\ \n"; @@ -239,11 +237,8 @@ let create_tmp_main_file modules = output_string oc "\"];;\n"; (* Initializes the kind of loading *) output_string oc (declare_loading_string()); - (* Start the right toplevel loop: Coq or Coq_searchisos *) - if !searchisos then - output_string oc "Cmd_searchisos_line.start();;\n" - else - output_string oc "Coqtop.start();;\n"; + (* Start the toplevel loop *) + output_string oc "Coqtop.start();;\n"; close_out oc; main_name with e -> |