From 2b2b10cd5bf017d9b69076ea98e4a1cb77fdbc00 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 1 Oct 2018 04:44:27 +0200
Subject: [dune] [configure] Fix typo in default prefix setting.

Fix silly typo that created havoc in developer out-of-the-box setups.
---
 configure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3