diff options
| author | Théo Zimmermann | 2018-10-01 13:25:41 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-01 13:25:41 +0200 |
| commit | e315f7b3e3e31eda27ef9f752d58aa85707f77bd (patch) | |
| tree | 03427beaec973659ca82e35ded2903aeb423329c | |
| parent | 6a800b15ebd26131f59605e9c8cdcd5bfec15f0d (diff) | |
| parent | 2b2b10cd5bf017d9b69076ea98e4a1cb77fdbc00 (diff) | |
Merge PR #8606: [dune] [configure] Fix typo in default prefix setting.
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index da6a6f8cbf..277c3d6439 100644 --- a/configure.ml +++ b/configure.ml @@ -1054,7 +1054,7 @@ let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout try Some (Sys.getenv "COQ_CONFIGURE_PREFIX") with | Not_found when !prefs.interactive -> None - | Not_found -> Some "_build/default/install" + | Not_found -> Some "_build/install/default" end | p -> p in match uservalue, env_prefix with |