diff options
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 *) |