diff options
| author | glondu | 2008-10-29 19:35:05 +0000 |
|---|---|---|
| committer | glondu | 2008-10-29 19:35:05 +0000 |
| commit | 3f9eb6ebe5217eaa929ef5632881460692e071f8 (patch) | |
| tree | e14c11d17545358dc24acd0d247cb2b5a459ea88 /scripts | |
| parent | f3f1b6cece86b785e1cf58fd5f1e273dbeceb92b (diff) | |
Remove calls to Dynlink.add_{interfaces,available_units} altogether
According to OCaml's Changes, all modules loaded so far (and
statically linked) are available to dynamically loaded modules (since
3.07). Therefore, these calls seem irrelevant now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11522 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqmktop.ml | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 021b1a80d0..320cbe1824 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -199,44 +199,10 @@ let clean file = rm (basename ^ ".cmx") end -(* Gives all modules in [dir]. Uses [.cmi] suffixes. Uses [Unix]. *) -let all_modules_in_dir dir = - try - let lst = ref [] - and dh = Unix.opendir dir in - try - while true do - let stg = Unix.readdir dh in - if (Filename.check_suffix stg ".cmi") then - lst := !lst @ [String.capitalize (Filename.chop_suffix stg ".cmi")] - done; - [] - with End_of_file -> - Unix.closedir dh; !lst - with Unix.Unix_error (_,"opendir",_) -> - failwith ("all_modules_in_dir: directory "^dir^" not found") - -(* Gives a part of command line (corresponding to dir) for [extract_crc] *) -let crc_cmd dir = - " -I "^dir^(List.fold_right (fun x y -> " "^x^y) (all_modules_in_dir dir) - "") - -(* Same as [crc_cmd] but recursively *) -let rec_crc_cmd dir = - List.fold_right (fun x y -> x^y) (List.map crc_cmd (all_subdirs dir)) "" - (* Creates another temporary file for Dynlink if needed *) let tmp_dynlink()= let tmp = Filename.temp_file "coqdynlink" ".ml" in let _ = Sys.command ("echo \"Dynlink.init();;\" > "^tmp) in - let _ = Sys.command (Coq_config.camllib^"/extract_crc"^(crc_cmd - Coq_config.camllib)^(crc_cmd Coq_config.camlp4lib)^(rec_crc_cmd - Coq_config.coqtop)^" >> "^tmp) in - let _ = Sys.command ("echo \";;\" >> "^tmp) in - let _ = - Sys.command ("echo \"Dynlink.add_available_units crc_unit_list;;\" >> "^ - tmp) - in tmp (* Initializes the kind of loading in the main program *) |
