From 308ea9a8d526160e2b45f16d63a0aee70984b814 Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Sun, 29 Sep 2019 19:33:29 +0200
Subject: [PATCH 08/13] Merge pull request #8996 from dra27/win-reconfigure

Windows supports make reconfigure now

(cherry picked from commit c71997a167c3670d202c6ecaf830c6a25b4b95b8)
---
 Makefile | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Makefile b/Makefile
index 7ac446f62..90583f1bc 100644
--- a/Makefile
+++ b/Makefile
@@ -326,11 +326,9 @@ endif
 utils/config.ml: utils/config.mlp Makefile.config utils/Makefile Makefile
 	$(MAKE) -C utils config.ml
 
-ifeq "$(UNIX_OR_WIN32)" "unix"
 .PHONY: reconfigure
 reconfigure:
 	./configure $(CONFIGURE_ARGS)
-endif
 
 .PHONY: partialclean
 partialclean::
-- 
2.23.0