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