32 lines
785 B
Diff
32 lines
785 B
Diff
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
|
|
|