Skip to content

Commit

Permalink
Add DUNE_PROFILE environment variable
Browse files Browse the repository at this point in the history
Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
  • Loading branch information
rgrinberg committed Feb 4, 2019
1 parent 5c9c1c0 commit 4389ce0
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 0 deletions.
3 changes: 3 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,9 @@ unreleased
was prepending paths and thus `$PKG_CONFIG_PATH` set by users could have been
overridden by homebrew installed libraries (#1785, @andreypopp)

- Add `DUNE_PROFILE` environment variable to easily set the profile. (..,
@rgrinberg)

1.6.2 (05/12/2018)
------------------

Expand Down
3 changes: 3 additions & 0 deletions bin/common.ml
Original file line number Diff line number Diff line change
Expand Up @@ -259,9 +259,12 @@ let term =
`Error
(true, "--dev is no longer accepted as it is now the default.")
and profile =
let doc =
"Build profile. dev if unspecified or release if -p is set." in
Arg.(value
& opt (some string) None
& info ["profile"] ~docs
~env:(Arg.env_var ~doc "DUNE_PROFILE")
~doc:
(sprintf
{|Select the build profile, for instance $(b,dev) or
Expand Down

0 comments on commit 4389ce0

Please sign in to comment.