From aca4cd47d2fe79c29b50f97888d0dc55b1d44f0d Mon Sep 17 00:00:00 2001
From: Jeremie Dimino <jeremie@dimino.org>
Date: Wed, 30 Aug 2017 00:43:31 +0100
Subject: [PATCH] Include Makefile.dev in Makefile

So that we can define a different default target while developping.
---
 .gitignore | 1 +
 Makefile   | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/.gitignore b/.gitignore
index 99af1064..4a81f652 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,3 +9,4 @@ boot.ml
 bootstrap.cmi
 bootstrap.cmo
 bootstrap.exe
+Makefile.dev
diff --git a/Makefile b/Makefile
index 1bfd4301..7bad65db 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,8 @@
 INSTALL_ARGS := $(if $(PREFIX),--prefix $(PREFIX),)
 BIN := ./_build/default/bin/main.exe
 
+-include Makefile.dev
+
 default: boot.exe
 	./boot.exe -j 4 --dev