From 473dd9b440fce3e27d8b1fe223d1961b716cac6d Mon Sep 17 00:00:00 2001
From: Jeremie Dimino <jeremie@dimino.org>
Date: Thu, 28 Jun 2018 12:40:27 +0100
Subject: [PATCH] Change the default build profile to dev during bootstrap

Signed-off-by: Jeremie Dimino <jeremie@dimino.org>
---
 src/main.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main.ml b/src/main.ml
index 22c8754f..f3cba367 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -267,7 +267,7 @@ let bootstrap () =
                              ; contexts = [Default { targets = [Native]
                                                    ; profile =
                                                        Option.value !profile
-                                                         ~default:"default"
+                                                         ~default:"dev"
                                                    }
                                           ]
                              }