Do not duplicate profile in missing deps message
Closes #1106 Signed-off-by: Etienne Millon <me@emillon.org>
This commit is contained in:
parent
ecd29a1c81
commit
f5c45a72a8
|
@ -6,6 +6,9 @@ next
|
|||
- Fix dune exec when `--build-dir` is set to an absolute path (#1105, fixes
|
||||
#1101, @rgrinberg)
|
||||
|
||||
- Fix duplicate profile argument in suggested command when an external library
|
||||
is missing (#1109, #1106, @emillon)
|
||||
|
||||
1.1.0 (06/08/2018)
|
||||
------------------
|
||||
|
||||
|
|
|
@ -510,8 +510,7 @@ let common =
|
|||
in
|
||||
let orig_args =
|
||||
List.concat
|
||||
[ dump_opt "--profile" profile
|
||||
; dump_opt "--workspace" (Option.map ~f:Arg.Path.arg workspace_file)
|
||||
[ dump_opt "--workspace" (Option.map ~f:Arg.Path.arg workspace_file)
|
||||
; orig
|
||||
]
|
||||
in
|
||||
|
|
|
@ -11,3 +11,19 @@ Reproduction case for #484. The error should point to src/jbuild
|
|||
Error: Library "a" not found.
|
||||
Hint: try: dune external-lib-deps --missing @install
|
||||
[1]
|
||||
|
||||
When passing --dev, the profile should be displayed only once (#1106):
|
||||
|
||||
$ jbuilder build --dev @install
|
||||
File "src/dune", line 4, characters 14-15:
|
||||
Error: Library "a" not found.
|
||||
Hint: try: dune external-lib-deps --missing --profile dev @install
|
||||
[1]
|
||||
|
||||
With dune and an explicit profile, it is the same:
|
||||
|
||||
$ dune build --profile dev @install
|
||||
File "src/dune", line 4, characters 14-15:
|
||||
Error: Library "a" not found.
|
||||
Hint: try: dune external-lib-deps --missing --profile dev @install
|
||||
[1]
|
||||
|
|
Loading…
Reference in New Issue