aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml2
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