Skip to content

Commit

Permalink
Fix Holmakefile INCLUDES error causing unnecessary HOL rebuilds
Browse files Browse the repository at this point in the history
You can't link back to src/ directories that precede boss because the
system imagines that the source files there depend on hol.state and
will promptly rebuild/recompile them, causing headaches later.
  • Loading branch information
mn200 committed Apr 19, 2024
1 parent ef4c2c8 commit 12c611b
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions examples/misc/Holmakefile
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
INCLUDES = $(dprot $(HOLDIR)/src/real) $(dprot $(HOLDIR)/src/real/analysis) \
$(dprot $(HOLDIR)/src/bag) $(dprot $(HOLDIR)/src/integer) \
$(dprot $(HOLDIR)/src/unwind)
$(dprot $(HOLDIR)/src/bag) $(dprot $(HOLDIR)/src/integer)

all: $(DEFAULT_TARGETS) euclid-OK thery-done
.PHONY: all
Expand Down

0 comments on commit 12c611b

Please sign in to comment.