Fix omitted dependency information in some Holmakefiles

Concurrent builds where stuff may or may not get linked to sigobj can mask a failure to explicitly depend on appropriate directories.
HOL-Theorem-Prover · Oct 25, 2023 · b0bf71b · b0bf71b
1 parent 871cc06
commit b0bf71b
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/src/n-bit/interactive_tests/Holmakefile b/src/n-bit/interactive_tests/Holmakefile
@@ -4,7 +4,7 @@ INCLUDES = ..
 
 all: test1 $(DEFAULT_TARGETS)
 
-test1: script1.ML
+test1: script1.ML ../wordsTheory.uo
 	$(protect $(HOLDIR)/bin/hol) $<
 
 

diff --git a/src/quotient/examples/lambda/Holmakefile b/src/quotient/examples/lambda/Holmakefile
@@ -1,3 +1,3 @@
-INCLUDES = .. ../../../string
+INCLUDES = .. ../../../string ../../../res_quan/src
 
 EXTRA_CLEANS = $(patsubst %,%.lst,alpha beta eta lift reduction term variable)
diff --git a/src/quotient/examples/sigma/Holmakefile b/src/quotient/examples/sigma/Holmakefile
@@ -1,3 +1,3 @@
-INCLUDES = .. ../../../string
+INCLUDES = .. ../../../string ../../../res_quan/src
 
 EXTRA_CLEANS = variable.lst