Skip to content

Commit b185432

Browse files
committed
Add DUNE_PROFILE environment variable
Signed-off-by: Rudi Grinberg <[email protected]>
1 parent 75661b4 commit b185432

File tree

2 files changed

+6
-0
lines changed

2 files changed

+6
-0
lines changed

CHANGES.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,9 @@ unreleased
127127
preprocessing actions
128128
(#1812, fixes #1811, @diml)
129129

130+
- Add `DUNE_PROFILE` environment variable to easily set the profile. (#1806,
131+
@rgrinberg)
132+
130133
1.6.2 (05/12/2018)
131134
------------------
132135

bin/common.ml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -259,9 +259,12 @@ let term =
259259
`Error
260260
(true, "--dev is no longer accepted as it is now the default.")
261261
and profile =
262+
let doc =
263+
"Build profile. dev if unspecified or release if -p is set." in
262264
Arg.(value
263265
& opt (some string) None
264266
& info ["profile"] ~docs
267+
~env:(Arg.env_var ~doc "DUNE_PROFILE")
265268
~doc:
266269
(sprintf
267270
{|Select the build profile, for instance $(b,dev) or

0 commit comments

Comments
 (0)