From aa981b320652a1dfea9147e2bd9dd3840561d717 Mon Sep 17 00:00:00 2001 From: Rudi Grinberg Date: Sat, 30 Jun 2018 17:19:16 +0700 Subject: [PATCH] Fix error message when workspace file doesn't exist Signed-off-by: Rudi Grinberg --- src/main.ml | 3 +++ test/blackbox-tests/test-cases/workspaces/run.t | 13 +------------ 2 files changed, 4 insertions(+), 12 deletions(-) diff --git a/src/main.ml b/src/main.ml index cc36328a..8c526b70 100644 --- a/src/main.ml +++ b/src/main.ml @@ -58,6 +58,9 @@ let setup ?(log=Log.no_log) | None -> match workspace_file with | Some p -> + if not (Path.exists p) then + die "@{Error@}: workspace file %s does not exist" + (Path.to_string_maybe_quoted p); Workspace.load ?x ?profile p | None -> match diff --git a/test/blackbox-tests/test-cases/workspaces/run.t b/test/blackbox-tests/test-cases/workspaces/run.t index 2c509561..376bcb56 100644 --- a/test/blackbox-tests/test-cases/workspaces/run.t +++ b/test/blackbox-tests/test-cases/workspaces/run.t @@ -25,18 +25,7 @@ analogously, jbuilder will ignore it specifying the workspace file is possible: $ dune build --root custom-workspace --workspace custom-workspace/dune-workspace.dev - Error: exception Sys_error("custom-workspace/dune-workspace.dev: No such file or directory") - Backtrace: - Raised by primitive operation at file "pervasives.ml", line 389, characters 28-54 - Called from file "src/stdune/io.ml", line 15, characters 15-35 - Called from file "src/main.ml", line 61, characters 8-36 - Called from file "src/main.ml", line 267, characters 12-56 - Called from file "bin/main.ml", line 756, characters 7-29 - Called from file "vendor/cmdliner/src/cmdliner_term.ml", line 27, characters 19-24 - Called from file "vendor/cmdliner/src/cmdliner.ml", line 106, characters 32-39 - Called from file "vendor/cmdliner/src/cmdliner.ml", line 136, characters 18-36 - Called from file "vendor/cmdliner/src/cmdliner.ml", line 251, characters 22-48 - Called from file "bin/main.ml", line 1562, characters 10-51 + Error: workspace file custom-workspace/dune-workspace.dev does not exist [1] Workspaces let you set custom profiles