diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 6 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 15 | ||||
| -rw-r--r-- | tools/coqc.ml | 2 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 2 | ||||
| -rw-r--r-- | tools/ocamllibdep.mll | 2 |
5 files changed, 13 insertions, 14 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8aff257386..5e223a0b48 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -39,7 +39,6 @@ CAMLP4BIN := $(COQMF_CAMLP4BIN) CAMLP4LIB := $(COQMF_CAMLP4LIB) CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) -COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) @CONF_FILE@: @PROJECT_FILE@ @COQ_MAKEFILE_INVOCATION@ @@ -404,7 +403,7 @@ uninstall:: instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \ rm -f "$$instf";\ echo RM "$$instf"; \ - rmdir --ignore-fail-on-non-empty "$(DESTDIR)$(COQLIBINSTALL)/$$df/"; \ + rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \ done .PHONY: uninstall @@ -414,8 +413,7 @@ uninstall-doc:: $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE)rmdir --ignore-fail-on-non-empty \ - "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" + $(HIDE) rmdir "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true .PHONY: uninstall-doc # Cleaning #################################################################### diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 8e2f75fc9c..e4f1359774 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -27,11 +27,6 @@ let rec print_prefix_list sep = function | x :: l -> print sep; print x; print_prefix_list sep l | [] -> () -(* These are the Coq library directories that are used for - * plugin development - *) -let lib_dirs = Envars.coq_src_subdirs - let usage () = output_string stderr "Usage summary:\ \n\ @@ -73,6 +68,7 @@ let usage () = \n[-f file]: take the contents of file as arguments\ \n[-o file]: output should go in file file\ \n Output file outside the current directory is forbidden.\ +\n[-bypass-API]: when compiling plugins, bypass Coq API\ \n[-h]: print this usage summary\ \n[--help]: equivalent to [-h]\n"; exit 1 @@ -197,9 +193,12 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) ;; -let generate_conf_coq_config oc args = +let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; - Envars.print_config ~prefix_var_name:"COQMF_" oc; + let src_dirs = if bypass_API + then Coq_config.all_src_dirs + else Coq_config.api_dirs @ Coq_config.plugins_dirs in + Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); ;; @@ -258,7 +257,7 @@ let generate_conf oc project args = fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); generate_conf_files oc project; generate_conf_includes oc project; - generate_conf_coq_config oc args; + generate_conf_coq_config oc args project.bypass_API; generate_conf_defs oc project; generate_conf_doc oc project; generate_conf_extra_target oc project.extra_targets; diff --git a/tools/coqc.ml b/tools/coqc.ml index 240531f123..c1f0182d9c 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -83,7 +83,7 @@ let parse_args () = | ("-config" | "--config") :: _ -> Envars.set_coqlib ~fail:(fun x -> x); - Envars.print_config stdout; + Envars.print_config stdout Coq_config.all_src_dirs; exit 0 |"--print-version" :: _ -> diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index cd04665cc1..9bca135127 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -265,7 +265,7 @@ let main () = (* Which ocaml compiler to invoke *) let prog = if !opt then "opt" else "ocamlc" in (* Which arguments ? *) - if !opt && !top then failwith "no custom toplevel in native code !"; + if !opt && !top then failwith "no custom toplevel in native code!"; let flags = if !opt then [] else Coq_config.vmbyteflags in let topstart = if !top then [ "topstart.cmo" ] else [] in let (modules, tolink) = files_to_link userfiles in diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll index f8b204c0b1..5d11e30089 100644 --- a/tools/ocamllibdep.mll +++ b/tools/ocamllibdep.mll @@ -28,6 +28,8 @@ let caml_up_ident = uppercase identchar* let caml_low_ident = lowercase identchar* rule mllib_list = parse + | uppercase+ { let s = Lexing.lexeme lexbuf in + s :: mllib_list lexbuf } | caml_up_ident { let s = uncapitalize (Lexing.lexeme lexbuf) in s :: mllib_list lexbuf } | "*predef*" { mllib_list lexbuf } |