From 5d54631d09fbe3110a3ef6862e2c66a5d0b9bb03 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 21 Feb 2021 13:16:50 -0800 Subject: [PATCH] [sledge] Fix `make debug` Summary: `make debug` should not be the same as `make release` Reviewed By: ngorogiannis Differential Revision: D26451307 fbshipit-source-id: 1bf924f92 --- sledge/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/sledge/Makefile b/sledge/Makefile index ab0c614cf..586b0676e 100644 --- a/sledge/Makefile +++ b/sledge/Makefile @@ -17,8 +17,8 @@ dune_install_release = dune install --context=release --prefix=_build/_install/r dune_build_trace = $(subst release,trace,$(dune_build_release)) dune_install_trace = $(subst release,trace,$(dune_install_release)) -dune_build_debug = $(subst debug,debug,$(dune_build_release)) -dune_install_debug = $(subst debug,debug,$(dune_install_release)) +dune_build_debug = $(subst release,debug,$(dune_build_release)) +dune_install_debug = $(subst release,debug,$(dune_install_release)) .PHONY: check check: