diff options
| author | Emilio Jesus Gallego Arias | 2018-11-06 11:33:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 06:37:05 +0100 |
| commit | 4e9bc09df64cd15e85c19ecabbc9580c00771176 (patch) | |
| tree | d5a9c68561a5d7573641053580b95bc3c7c9be43 /tools/coq_makefile.ml | |
| parent | f8a76b3d383abf468fb21df509f5da8f8aafa913 (diff) | |
[CoqProject] Abstract warning function for CoqProject readers.
`CoqProject_file` uses the feedback system, however this is not very
convenient in some scenarios such as `coqdep` that has to be run very
early in the build process [and thus in "boot" mode].
We thus make the warning function a paramater.
Should fix #8913.
Diffstat (limited to 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ca5a232edb..8560bac786 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -396,8 +396,9 @@ let _ = | "-destination-of" :: tgt :: rest -> Some tgt, rest | _ -> None, args in - let project = - try cmdline_args_to_project ~curdir:Filename.current_dir_name args + let project = + let warning_fn x = Format.eprintf "%s@\n%!" x in + try cmdline_args_to_project ~warning_fn ~curdir:Filename.current_dir_name args with Parsing_error s -> prerr_endline s; usage_coq_makefile () in if only_destination <> None then begin |