Include Makefile.dev in Makefile

So that we can define a different default target while developping.
2017-08-30 00:43:31 +01:00 · 2017-08-30 00:43:31 +01:00 · aca4cd47d2
parent 47d1f74ef0
commit aca4cd47d2
2 changed files with 3 additions and 0 deletions
--- a/.gitignore
+++ b/.gitignore
@ -9,3 +9,4 @@ boot.ml
 bootstrap.cmi
 bootstrap.cmo
 bootstrap.exe
+Makefile.dev
--- a/2
+++ b/2
@ -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