diff options
| author | Emilio Jesus Gallego Arias | 2018-10-01 04:44:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-01 04:44:27 +0200 |
| commit | 2b2b10cd5bf017d9b69076ea98e4a1cb77fdbc00 (patch) | |
| tree | 5b9900d901959f65dcaf09df04e8448caca3f4a0 /configure.ml | |
| parent | c155259dee7e4b2bfafe42375b45f2f4d6c6cfbd (diff) | |
[dune] [configure] Fix typo in default prefix setting.
Fix silly typo that created havoc in developer out-of-the-box setups.
Diffstat (limited to 'configure.ml')
| -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 |