diff options
Diffstat (limited to 'tools')
-rw-r--r-- | tools/CoqMakefile.in | 10 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 4 | ||||
-rw-r--r-- | tools/coqdoc/index.ml | 2 | ||||
-rw-r--r-- | tools/coqdoc/index.mli | 2 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 4 |
5 files changed, 11 insertions, 11 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index deb92e728..2ebe4aba7 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -65,20 +65,20 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -# Use /usr/bin/env time on linux, gtime on Mac OS +# Use command time on linux, gtime on Mac OS TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) else ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else -STDTIME?=time +STDTIME?=command time endif endif else -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +STDTIME?=command time -f $(TIMEFMT) endif # Coq binaries diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 6f11ee397..ad489da82 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -218,7 +218,7 @@ let windrive s = else "" ;; -let generate_conf_coq_config oc args = +let generate_conf_coq_config oc = section oc "Coq configuration."; let src_dirs = Coq_config.all_src_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; @@ -282,7 +282,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; generate_conf_defs oc project; generate_conf_doc oc project; generate_conf_extra_target oc project.extra_targets; diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index df493fdf7..885324aa0 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -77,7 +77,7 @@ let add_ref m loc m' sp id ty = let find m l = Hashtbl.find reftable (m, l) -let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) +let find_string s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) (* Coq modules *) diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 5cd301389..7c9aad67f 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -41,7 +41,7 @@ type index_entry = val find : coq_module -> loc -> index_entry (* Find what data is referred to by some string in some coq module *) -val find_string : coq_module -> string -> index_entry +val find_string : string -> index_entry val add_module : coq_module -> unit diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d25227002..c640167ac 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -431,7 +431,7 @@ module Latex = struct else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then try - let tag = Index.find_string (get_module false) s in + let tag = Index.find_string s in reference (translate s) tag with _ -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s @@ -706,7 +706,7 @@ module Html = struct else if is_keyword s then printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then - try reference (translate s) (Index.find_string (get_module false) s) + try reference (translate s) (Index.find_string s) with Not_found -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s |