From 59aa19ab9adc2c8aceaa7752d5fecb24ebe2d725 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 9 Dec 2019 18:05:45 +0100
Subject: [build] Allow the selection of build system using an env var.

This is undocumented on purpose by now.

Suggested by Gaëtan Gilbert
---
 Makefile | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 635885b191..c416172dbf 100644
--- a/Makefile
+++ b/Makefile
@@ -9,4 +9,8 @@
 ##########################################################################
 
 # The default build system is make-based one.
+ifndef COQ_USE_DUNE
 include Makefile.make
+else
+include Makefile.dune
+endif
-- 
cgit v1.2.3