diff options
| author | Emilio Jesus Gallego Arias | 2018-10-01 05:19:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-11 14:32:13 +0200 |
| commit | dc5dbc992727fb807fa56763f8f71d79f598fd6a (patch) | |
| tree | 494f0e418e6da50fc630d33700ac5376effc6680 /configure.ml | |
| parent | aa5cdbd67b160417fe353a79393a89ed99481548 (diff) | |
[configure] Use absolute path for prefix.
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 7cc58a3506..f884a7de5c 100644 --- a/configure.ml +++ b/configure.ml @@ -1038,7 +1038,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/install/default" + | Not_found -> Some Sys.(getcwd () ^ "/../install/default") end | p -> p in match uservalue, env_prefix with |