don't use wildcard match where not necessary
Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
This commit is contained in:
parent
2b307bfe99
commit
989a1c0058
|
@ -59,7 +59,7 @@ let setup ?(log=Log.no_log)
|
||||||
match workspace_file with
|
match workspace_file with
|
||||||
| Some p ->
|
| Some p ->
|
||||||
Workspace.load ?x ?profile p
|
Workspace.load ?x ?profile p
|
||||||
| _ ->
|
| None ->
|
||||||
match
|
match
|
||||||
let p = Path.of_string Workspace.filename in
|
let p = Path.of_string Workspace.filename in
|
||||||
Option.some_if (Path.exists p) p
|
Option.some_if (Path.exists p) p
|
||||||
|
|
Loading…
Reference in New Issue