diff options
| author | Emilio Jesus Gallego Arias | 2020-02-13 00:24:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-13 22:11:05 +0100 |
| commit | 4ea2825a4589b0c77225dd6f4caf98b12ac6dd6f (patch) | |
| tree | bff1d2d38f7e8dbc6f55506e8bcc1e8fc7821948 /tools | |
| parent | 2e36df827c85ea93cc7614dc25f82a16f72e6e9d (diff) | |
[coqdep] Merge `-sort` and `-suffix` options.
They are always used together, no other use case of `-suffix` that I
can see.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 4 | ||||
| -rw-r--r-- | tools/coqdep.ml | 3 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 10 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 1 |
4 files changed, 6 insertions, 12 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index d3ed5e78b4..81ccf2c283 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -455,13 +455,13 @@ all.ps: $(VFILES) $(SHOW)'COQDOC -ps $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` all.pdf: $(VFILES) $(SHOW)'COQDOC -pdf $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` # FIXME: not quite right, since the output name is different gallinahtml: GAL=-g diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 950c784325..23cc83b8d3 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -44,7 +44,6 @@ let usage () = eprintf " -vos : also output dependencies about .vos files\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 @@ -81,8 +80,6 @@ let rec parse = function | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: s :: ll -> suffixe := s ; parse ll - | "-suffix" :: [] -> usage () | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 5ece595f13..07841abad9 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -38,8 +38,6 @@ let option_boot = ref false let norec_dirs = ref StrSet.empty -let suffixe = ref ".vo" - type dir = string option (** [get_extension f l] checks whether [f] has one of the extensions @@ -498,10 +496,10 @@ let coq_dependencies () = List.iter (fun (name,_) -> let ename = escape name in - let glob = if !option_noglob then "" else " "^ename^".glob" in + let glob = if !option_noglob then "" else ename^".glob " in let deps = find_dependencies name in - printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename - (string_of_dependency_list !suffixe deps); + printf "%s.vo %s%s.v.beautified %s.required_vo: %s.v %s\n" ename glob ename ename ename + (string_of_dependency_list ".vo" deps); printf "%s.vio: %s.v %s\n" ename ename (string_of_dependency_list ".vio" deps); if !write_vos then @@ -639,7 +637,7 @@ let sort () = done with Fin_fichier -> close_in cin; - printf "%s%s " file !suffixe + printf "%s.v " file end in List.iter (fun (name,_) -> loop name) !vAccu diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 1820db4a1e..cb436f7f02 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -25,7 +25,6 @@ val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref val write_vos : bool ref -val suffixe : string ref type dynlink = Opt | Byte | Both | No | Variable val option_dynlink : dynlink ref |