[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
master
Josh Berdine 4 years ago committed by Facebook GitHub Bot
parent 02ab2f18c9
commit 5d54631d09

@ -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:

Loading…
Cancel
Save