Skip to content

Commit

Permalink
Fix the target all of the Makefile (#914)
Browse files Browse the repository at this point in the history
The PR #887 was wrong... The target @check of `Dune` doesn't build
all the binaries, it builds only binary artefacts `cmi`, `cmx`, ... but
no linkage is performed.

This commit mostly reverts the changes. As the sources are located in
`src/`, I use the target `@src/all`. Now the command `make` will build
everything in the directory `src`. I also add `examples` since we want
to check the libusage module still compile.
  • Loading branch information
Halbaroth authored Oct 19, 2023
1 parent dcb94b0 commit a70c6fc
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,8 @@ plugins:
# Hopefully more efficient than making "all" depend
# on "lib" and "bin", since dune can parralelize more
all:
$(DUNE) build $(DUNE_FLAGS) @check
$(DUNE) build $(DUNE_FLAGS) @$(SRC_DIR)/all @examples/all
ln -sf src/bin/text/Main_text.exe alt-ergo

# declare these targets as phony to avoid name clashes with existing directories,
# particularly the "plugins" target
Expand Down

0 comments on commit a70c6fc

Please sign in to comment.