From 0d45f7ba376702a0ab6ec34625761c3f9c26a519 Mon Sep 17 00:00:00 2001 From: Mark Shinwell Date: Wed, 28 Aug 2024 10:29:42 +0100 Subject: [PATCH] Disable minimizer-upstream (#2981) (cherry picked from commit bf147244af320e471cdbb4e0c26d88860edd9c5d) --- Makefile | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index e9b4d37060a..1f12b02a9f0 100644 --- a/Makefile +++ b/Makefile @@ -24,15 +24,16 @@ ci: ci-no-coverage endif .PHONY: ci-no-coverage -ci-no-coverage: runtest runtest-upstream minimizer-upstream minimizer +ci-no-coverage: runtest runtest-upstream minimizer .PHONY: ci-coverage ci-coverage: boot-runtest coverage -.PHONY: minimizer-upstream -minimizer-upstream: - cp chamelon/dune.upstream chamelon/dune - RUNTIME_DIR=$(RUNTIME_DIR) $(dune) build $(ws_boot) @chamelon/all +# CR mshinwell: build is broken +# .PHONY: minimizer-upstream +# minimizer-upstream: +# cp chamelon/dune.upstream chamelon/dune +# RUNTIME_DIR=$(RUNTIME_DIR) $(dune) build $(ws_main) @chamelon/all .PHONY: minimizer minimizer: _build/_bootinstall