Skip to content

Commit

Permalink
Make the makefile compatible with dune >= 2.9.1
Browse files Browse the repository at this point in the history
  • Loading branch information
kit-ty-kate committed Mar 5, 2024
1 parent d25e1e1 commit d33f5b4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ else
DUNE_EXE=
# NB make does not export the PATH update in Makefile.config to $(shell ...)
ifeq ($(shell PATH='$(PATH)' $(DUNE) build --root . --help=plain 2>/dev/null \
| grep -F -- '$(DUNE_PROMOTE_ARG) '),)
| grep -F -- '$(DUNE_PROMOTE_ARG)'),)
DUNE_PROMOTE_ARG =
endif
endif
Expand Down

0 comments on commit d33f5b4

Please sign in to comment.