diff options
| author | Enrico Tassi | 2019-02-22 20:52:14 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-02-22 20:52:14 +0100 |
| commit | dea9f08178efcf9cfac7ee2970dc21abc2fde308 (patch) | |
| tree | 515a3caec0fd881b71ac1cdbab743cfb5fd473bf /tools | |
| parent | 6a289e4fbc1c4327429bb7041e8f39a18bbb0f70 (diff) | |
| parent | e8419bac30ab98527ec6b15d5a0f5c1035539ca5 (diff) | |
Merge PR #9576: [library] Remove `-boot` option.
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_dune.ml | 2 | ||||
| -rw-r--r-- | tools/coq_tex.ml | 3 |
2 files changed, 1 insertions, 4 deletions
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index 68371edcb1..62a871aa0e 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -186,7 +186,7 @@ let pp_vo_dep dir fmt vo = (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) let libflag = "-coqlib %{project_root}" in (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqc -boot %s %s %s %s))" libflag eflag cflag source in + let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in let all_targets = gen_coqc_targets vo in pp_rule fmt all_targets deps action diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index 0ffa5bd7e4..c6d3551561 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -259,8 +259,6 @@ let parse_cl () = " Coq parts are written between 2 horizontal lines"; "-small", Arg.Set small, " Coq parts are written in small font"; - "-boot", Arg.Set boot, - " Launch coqtop with the -boot option" ] (fun s -> files := s :: !files) "coq-tex [options] file ..." @@ -279,7 +277,6 @@ let find_coqtop () = let _ = parse_cl (); if !image = "" then image := Filename.quote (find_coqtop ()); - if !boot then image := !image ^ " -boot"; if Sys.command (!image ^ " -batch -silent") <> 0 then begin Printf.printf "Error: "; let _ = Sys.command (!image ^ " -batch") in |