Coqmktop: missing -I (fix #2851)

 The modules used in coqmktop's temporary main file should have
 their .cmi in the search path, hence a small set of -I is required:
 lib, toplevel. We do not place their the full list to avoid issues
 with the win32 command-line length

 Btw, coqmktop -boot now also builds its list of -I instead of receiving
 them via its command-line, it's simpler this way...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 7 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 230ab75928..441926becf 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -63,16 +63,18 @@ let no_start   = ref false
 
 let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
 
+(* Since the .cma are given with their relative paths (e.g. "lib/clib.cma"),
+   we only need to include directories mentionned in the temp main ml file
+   below (for accessing the corresponding .cmi). *)
+
 let src_dirs =
-  [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ]
+  [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]  ]
 
 let includes () =
-  (if !Flags.boot then [] (* the include flags are given on the cmdline *)
-   else
-      let coqlib = Envars.coqlib Errors.error in
-      let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
-      let camlp4incl = ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""] in
-      List.fold_right (fun d l -> "-I" :: mkdir d :: l)	src_dirs camlp4incl)
+  let coqlib = if !Flags.boot then "." else Envars.coqlib Errors.error in
+  let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
+  (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
+  @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
   @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
 
 (* Transform bytecode object file names in native object file names *)