From b92270125c6cd88170facf5fe980894964296777 Mon Sep 17 00:00:00 2001
From: Niklas Larsson <niklas@mm.st>
Date: Wed, 17 Jun 2020 14:31:17 +0200
Subject: [PATCH] Use custom configuration from custom.mk if present.

---
 .gitignore | 2 ++
 config.mk  | 3 +++
 2 files changed, 5 insertions(+)

diff --git a/.gitignore b/.gitignore
index 7210bd79f..04997db83 100644
--- a/.gitignore
+++ b/.gitignore
@@ -34,3 +34,5 @@ idris2docs_venv
 /bootstrap/idris2_app/libidris2_support.*
 /bootstrap/idris2boot
 /bootstrap/idris2boot.rkt
+
+/custom.mk
\ No newline at end of file
diff --git a/config.mk b/config.mk
index 9c7148730..1aec67606 100644
--- a/config.mk
+++ b/config.mk
@@ -44,3 +44,6 @@ ifeq ($(OS),bsd)
 else
 	MAKE := make
 endif
+
+# Add a custom.mk file to override any of the configurations
+-include custom.mk